CubicPathwidth.Alg.Proofs2.D1KeyStepAt

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

import CubicPathwidth.Alg.Plan2
import CubicPathwidth.T4.DeletionXKey
import CubicPathwidth.T4.TorsoDyn

/-!
# Stage 2 task D1: one round of the deletion process (`KeyStepAt`)

Copy-edit of `CubicPathwidth.T4.DelX.key_step` (`T4/DeletionXKey.lean`), with the
hypotheses of `KeyStepAt` (Plan2.lean, §6):

* non-basicness is dropped: the vertex `w` (a vertex of maximum torso degree on `C`
  with a neighbour of smaller degree, or `C` regular), the reduced core `B'` and a
  surviving vertex `u ∈ B' ∩ C` are hypotheses;
* the deletion of `w` followed by the reduction-only `Reach` to `(F.erase w, B')` is
  given; the degree bound `tdeg (F.erase w) B' ≤ tdeg (F.erase w) (B.erase w)` on `B'`
  (needed by `DelX.claim_J`) is proved here (`D1.reach_red_aux`), by induction on the
  `Reach` with `T4.tdeg_erase_le`;
* the remaining arithmetic (`DelX.claim_J`, `DelX.deletion_core_ineq`, `DelX.psi_delete`)
  is imported from `T4.DeletionXKey` and `T4.DeletionXArith`, unchanged.

`torsoDynamics` (`T4/TorsoDyn.lean`) supplies the torso semantics.
-/

noncomputable section

namespace CubicPathwidth.Alg

namespace D1

variable {n : ℕ}

/-- Along a `Reach` from a good state `(F, B)` back to the same deleted set `F`, the core
only shrinks and torso degrees (on the core) do not increase. The induction is on the
`Reach`; a deletion step cannot end at the same undeleted set, since the deleted vertex
would lie in `F` and not in `F`. -/
theorem reach_red_aux {G : SimpleGraph (Fin n)} {F B : Finset (Fin n)}
    (hg : T4.Good G F B) {t : Finset (Fin n) × Finset (Fin n)}
    (hr : T4.Reach G (F, B) t) :
    t.1 = F → t.2 ⊆ B ∧ ∀ v ∈ t.2, T4.tdeg G F t.2 v ≤ T4.tdeg G F B v := by
  induction hr with
  | refl => intro _; exact ⟨Finset.Subset.rfl, fun _ _ => le_rfl⟩
  | tail hab hbc ih =>
    rename_i s' t'
    obtain ⟨F1, B1⟩ := s'
    obtain ⟨F2, B2⟩ := t'
    intro ht
    have hgs : T4.Good G F1 B1 := hg.reach hab
    have hsubF : F1 ⊆ F := (T4.Reach.subset hab).1
    cases hbc with
    | @reduce _ _ v hv hd =>
      have hF1 : F1 = F := ht
      obtain ⟨h1, h2⟩ := ih hF1
      show B1.erase v ⊆ B ∧ ∀ u ∈ B1.erase v, T4.tdeg G F (B1.erase v) u ≤ T4.tdeg G F B u
      refine ⟨(Finset.erase_subset _ _).trans h1, fun u hu => ?_⟩
      have hB1F : B1 ⊆ F1 := hgs.subset
      have hd1 : T4.tdeg G F1 B1 v ≤ 2 := hd
      have hle := T4.tdeg_erase_le G hB1F hv hd1 hu
      rw [hF1] at hle
      exact hle.trans (h2 u (Finset.mem_of_mem_erase hu))
    | @delete _ _ w hw =>
      exfalso
      have hwF1 : w ∈ F1 := hgs.subset hw
      have hwF : w ∈ F := hsubF hwF1
      have ht' : F1.erase w = F := ht
      have : w ∈ F1.erase w := by rw [ht']; exact hwF
      exact (Finset.notMem_erase w F1) this

/-- Degrees on the reduced core do not increase along a reduction-only `Reach`. -/
theorem reach_red_deg {G : SimpleGraph (Fin n)} {F B B' : Finset (Fin n)}
    (hg : T4.Good G F B) (hr : T4.Reach G (F, B) (F, B')) :
    B' ⊆ B ∧ ∀ v ∈ B', T4.tdeg G F B' v ≤ T4.tdeg G F B v :=
  reach_red_aux hg hr rfl

end D1

/-- Task D1: `KeyStepAt` (one round of the deletion process on a non-basic component,
with the centre `w`, the reduced core `B'` and the surviving vertex as hypotheses). -/
theorem keyStepAt : KeyStepAt := by
  classical
  unfold KeyStepAt
  intro b hb n G F B C B' w hg hmin hC hwC hmax h6 hreg hB'sub hR hmin' hsurv
  have hdyn : T4.TorsoDynamics := T4.torsoDynamics
  obtain ⟨hCB, hcl, hconn⟩ := mem_components (T4.tgraph G F B) hC
  have hCne : C.Nonempty := hconn.1
  have hwB : w ∈ B := hCB hwC
  have hstep : T4.Step G (F, B) (F.erase w, B.erase w) := T4.Step.delete hwB
  have hg1 : T4.Good G (F.erase w) (B.erase w) := hg.reach (T4.Reach.single hstep)
  have hRfull : T4.Reach G (F, B) (F.erase w, B') := (T4.Reach.single hstep).trans hR
  have hdeg' : ∀ v ∈ B', T4.tdeg G (F.erase w) B' v ≤ T4.tdeg G (F.erase w) (B.erase w) v :=
    (D1.reach_red_deg hg1 hR).2
  obtain ⟨u₁, hu₁B', hu₁C⟩ := hsurv
  have hCd : ∀ v ∈ C, 3 ≤ T4.tdeg G F B v ∧ T4.tdeg G F B v ≤ T4.tdeg G F B w :=
    fun v hv => ⟨hmin v (hCB hv), hmax v hv⟩
  have hNC : T4.DelX.nbrs G F B w ⊆ C.erase w := by
    intro u hu
    have h := T4.DelX.mem_nbrs.mp hu
    refine Finset.mem_erase.mpr ⟨h.1.symm, ?_⟩
    exact hcl w hwC u h.2.2.1 h
  have hNcard : (T4.DelX.nbrs G F B w).card = T4.tdeg G F B w :=
    (T4.DelX.tdeg_eq_card_nbrs G F B w).symm
  have hd'N : ∀ v ∈ T4.DelX.nbrs G F B w,
      T4.tdeg G (F.erase w) (B.erase w) v + 1 = T4.tdeg G F B v := by
    intro v hv
    have hvw : v ≠ w := Finset.ne_of_mem_erase (T4.DelX.nbrs_subset_erase hv)
    have := T4.DelX.tdeg_delete hdyn hg hwB hvw
    simpa [hv] using this
  have hd'o : ∀ v ∈ C.erase w, v ∉ T4.DelX.nbrs G F B w →
      T4.tdeg G (F.erase w) (B.erase w) v = T4.tdeg G F B v := by
    intro v hv hvn
    have hvw : v ≠ w := Finset.ne_of_mem_erase hv
    have := T4.DelX.tdeg_delete hdyn hg hwB hvw
    simpa [hvn] using this
  have hδ : ∀ v ∈ C, T4.cmin G F B C ≤ T4.tdeg G F B v := by
    intro v hv
    unfold T4.cmin
    simp only [hCne, dite_true]
    exact Finset.inf'_le _ hv
  have hδ' : ∃ v ∈ C, T4.tdeg G F B v = T4.cmin G F B C := by
    unfold T4.cmin
    simp only [hCne, dite_true]
    obtain ⟨v, hv, h⟩ := Finset.exists_mem_eq_inf' hCne (T4.tdeg G F B)
    exact ⟨v, hv, h.symm⟩
  have hreg' : (∀ v ∈ C, T4.tdeg G F B v = T4.tdeg G F B w) ∨
      ∃ x ∈ T4.DelX.nbrs G F B w, T4.tdeg G F B x < T4.tdeg G F B w := by
    rcases hreg with h | ⟨x, hx, hxlt⟩
    · exact Or.inl h
    · exact Or.inr ⟨x, T4.DelX.mem_nbrs.mpr hx, hxlt⟩
  have hJ := T4.DelX.claim_J hdyn hb hg hmin hC hwC hB'sub hRfull hdeg'
  have hstar : ∃ u ∈ C.erase w, 3 ≤ T4.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 := T4.DelX.deletion_core_ineq hb C (T4.DelX.nbrs G F B w) w (T4.tdeg G F B)
    (T4.tdeg G (F.erase w) (B.erase w)) (T4.tdeg G F B w) (T4.cmin G F B C)
    (T4.DelX.Jval b G F B C w B') h6 hCd rfl hNC hNcard hd'N hd'o hδ hδ' hreg' hJ hstar
  have hid := hb.identity (T4.tdeg G F B w) h6
  have hpd := T4.DelX.psi_delete hdyn b hg hwB
  have hcsum : ∑ D ∈ T4.tcomps G F B, T4.runMin b (T4.cmin G F B D) =
      T4.runMin b (T4.cmin G F B C) +
        ∑ D ∈ (T4.tcomps G F B).erase C, T4.runMin b (T4.cmin G F B D) :=
    (Finset.add_sum_erase _ _ hC).symm
  unfold T4.psiMinus
  rw [hcsum]
  unfold T4.DelX.Jval at hcore
  have hincr : ∀ v, b (T4.tdeg G F B v) - b (T4.tdeg G F B v - 1) =
      T4.incr b (T4.tdeg G F B v) :=
    fun v => rfl
  simp only [hincr] at hpd
  linarith

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.keyStepAt