CubicPathwidth.T4.DeletionX

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

import CubicPathwidth.T4.DeletionXKey

/-!
# The deletion process (`prop:deletion`, base degree `k = 5`)

`deletion_x : DeletionClaim` follows the proof of Proposition 9.10 (`prop:deletion`). The induction is on the size of the
core. If every torso component is basic, the empty sequence works. Otherwise
`DelX.key_step` (`DeletionXKey.lean`) deletes a vertex `w` of a non-basic component
(a vertex of maximum torso degree, preferably with a neighbour of smaller degree),
reduces maximally (`TorsoDynamics`, part 3), and shows `1 + ψ⁻' ≤ ψ⁻`: the rewriting
into `J₁ + J₂ + J₃ + J₄`, the Claim on `J₄` (`DelX.claim_J`) and the cases 1, 2a, 2b of
the manuscript (`DelX.deletion_core_ineq`, `DeletionXArith.lean`). The "disconnected"
case of the manuscript is not a separate case here: the other torso components survive
the round unchanged (`DelX.tcomp_preserve`) and cancel in `ψ⁻` (`DelX.comp_sum_ge`).
-/

noncomputable section

namespace CubicPathwidth
namespace T4

open T2 SectionDecomposition

theorem deletion_x : DeletionClaim := by
  classical
  intro hdyn b hb n G
  suffices h : ∀ m : ℕ, ∀ F B : Finset (Fin n), B.card = m → Good G F B →
      (∀ v ∈ B, 3 ≤ tdeg G F B v) →
      ∃ F' B' : Finset (Fin n), Reach G (F, B) (F', B') ∧
        (∀ v ∈ B', 3 ≤ tdeg G F' B' v) ∧
        (∀ C ∈ tcomps G F' B', Basic G F' B' C) ∧
        ((F \ F').card : ℝ) + psiMinus b G F' B' ≤ psiMinus b G F B by
    intro F B hg hmin
    exact h B.card F B rfl hg hmin
  intro m
  induction m using Nat.strong_induction_on with
  | _ m ih =>
    intro F B hcard hg hmin
    by_cases hall : ∀ C ∈ tcomps G F B, Basic G F B C
    · exact ⟨F, B, Reach.refl G _, hmin, hall, by simp⟩
    · have hex : ∃ C ∈ tcomps G F B, ¬ Basic G F B C := by
        by_contra h
        exact hall fun C hC => by_contra fun hn => h ⟨C, hC, hn⟩
      obtain ⟨C, hC, hnb⟩ := hex
      obtain ⟨w, hwB, B', hB'sub, hR, hmin', hpot⟩ :=
        DelX.key_step hdyn hb hg hmin hC hnb
      have hlt : B'.card < m := by
        have h1 : B'.card ≤ (B.erase w).card := Finset.card_le_card hB'sub
        have h2 : (B.erase w).card < B.card := Finset.card_erase_lt_of_mem hwB
        omega
      obtain ⟨F', B'', hR', hmin'', hbasic, hpot'⟩ :=
        ih B'.card hlt (F.erase w) B' rfl (hg.reach hR) hmin'
      refine ⟨F', B'', hR.trans hR', hmin'', hbasic, ?_⟩
      have hwF : w ∈ F := hg.subset hwB
      have hF'sub : F' ⊆ F.erase w := (Reach.subset hR').1
      have hset : F \ F' = insert w ((F.erase w) \ F') := by
        ext x
        simp only [Finset.mem_sdiff, Finset.mem_erase, Finset.mem_insert]
        constructor
        · rintro ⟨hxF, hxF'⟩
          by_cases hxw : x = w
          · exact Or.inl hxw
          · exact Or.inr ⟨⟨hxw, hxF⟩, hxF'⟩
        · rintro (rfl | ⟨⟨hxw, hxF⟩, hxF'⟩)
          · exact ⟨hwF, fun h => by have := hF'sub h; simp at this⟩
          · exact ⟨hxF, hxF'⟩
      have hnot : w ∉ (F.erase w) \ F' := by simp
      have hcardF : (F \ F').card = ((F.erase w) \ F').card + 1 := by
        rw [hset, Finset.card_insert_of_notMem hnot]
      rw [hcardF]
      push_cast
      linarith

end T4
end CubicPathwidth

#print axioms CubicPathwidth.T4.deletion_x
Back to top