CubicPathwidth.T3.Charging5

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

import CubicPathwidth.T3.Defs
import CubicPathwidth.T2.Charging

/-!
# Charging along edges joining degrees 3, 4 and 5 (claim C3)

Proves `Charging5Claim`: under the per-vertex charging inequalities, the total charge
is at most `a₃ n₃ + a₄ n₄ + a₅ n₅`. The transfer terms cancel in pairs by the double
count of edges joining two different degrees in `{3,4,5}`.
-/

noncomputable section
open scoped Classical

namespace CubicPathwidth
namespace T3

open Finset T2

/-- Double count for any pair of degrees `p`, `q`: the edges joining a vertex of degree
`p` to one of degree `q` are counted the same way from both ends. -/
lemma edge_double_count_pq {n : ℕ} (G : SimpleGraph (Fin n)) (p q : ℕ) :
    ∑ v, (if G.degree v = p then (nbrCount G v q : ℝ) else 0) =
      ∑ u, (if G.degree u = q then (nbrCount G u p : ℝ) else 0) := by
  classical
  have hL : ∀ v : Fin n,
      (if G.degree v = p then (nbrCount G v q : ℝ) else 0) =
        ∑ u, if G.degree v = p ∧ G.Adj v u ∧ G.degree u = q then (1 : ℝ) else 0 := by
    intro v
    rw [nbrCount_cast_eq]
    split_ifs with h
    · simp [h]
    · simp [h]
  have hR : ∀ u : Fin n,
      (if G.degree u = q then (nbrCount G u p : ℝ) else 0) =
        ∑ v, if G.degree v = p ∧ G.Adj v u ∧ G.degree u = q then (1 : ℝ) else 0 := by
    intro u
    rw [nbrCount_cast_eq]
    split_ifs with h
    · refine Finset.sum_congr rfl fun v _ => ?_
      by_cases h1 : G.Adj v u
      · have h1' := h1.symm
        by_cases h2 : G.degree v = p <;> simp [h, h1, h1', h2]
      · have h1' : ¬G.Adj u v := fun h' => h1 h'.symm
        by_cases h2 : G.degree v = p <;> simp [h, h1, h1', h2]
    · simp [h]
  simp_rw [hL, hR]
  exact Finset.sum_comm

/-- Every vertex has degree 3, 4 or 5 when the minimum degree is at least 3 and the
maximum degree is at most 5. -/
lemma degree_cases {n : ℕ} {G : SimpleGraph (Fin n)} (hmin : MinDegreeAtLeast 3 G)
    (hmax : MaxDegreeAtMost 5 G) (v : Fin n) :
    G.degree v = 3 ∨ G.degree v = 4 ∨ G.degree v = 5 := by
  unfold MinDegreeAtLeast at hmin
  unfold MaxDegreeAtMost at hmax
  have h1 := hmin v
  have h2 := hmax v
  omega

theorem charging5 : Charging5Claim := by
  classical
  unfold Charging5Claim
  intro n G hmin hmax C a₃ a₄ a₅ t₃₄ t₃₅ t₄₅ h
  have hdeg : ∀ v : Fin n, G.degree v = 3 ∨ G.degree v = 4 ∨ G.degree v = 5 :=
    fun v => degree_cases hmin hmax v
  -- per-vertex expansion of the transfer term as a combination of the three transfers
  have key : ∀ v : Fin n,
      transferTerm (G.degree v) (nbrCount G v 3) (nbrCount G v 4) (nbrCount G v 5)
          t₃₄ t₃₅ t₄₅ =
        t₃₄ * ((if G.degree v = 4 then (nbrCount G v 3 : ℝ) else 0) -
            (if G.degree v = 3 then (nbrCount G v 4 : ℝ) else 0)) +
        t₃₅ * ((if G.degree v = 5 then (nbrCount G v 3 : ℝ) else 0) -
            (if G.degree v = 3 then (nbrCount G v 5 : ℝ) else 0)) +
        t₄₅ * ((if G.degree v = 5 then (nbrCount G v 4 : ℝ) else 0) -
            (if G.degree v = 4 then (nbrCount G v 5 : ℝ) else 0)) := by
    intro v
    rcases hdeg v with h' | h' | h' <;> simp [transferTerm, h'] <;> ring
  -- the transfer terms cancel by the three double counts
  have hsum : ∑ v, transferTerm (G.degree v) (nbrCount G v 3) (nbrCount G v 4)
      (nbrCount G v 5) t₃₄ t₃₅ t₄₅ = 0 := by
    rw [Finset.sum_congr rfl fun v _ => key v]
    simp only [Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_sub_distrib]
    have e1 := edge_double_count_pq G 4 3
    have e2 := edge_double_count_pq G 5 3
    have e3 := edge_double_count_pq G 5 4
    linear_combination t₃₄ * e1 + t₃₅ * e2 + t₄₅ * e3
  -- the coefficients add up to the degree-count form
  have hcoeff : ∑ v, coeff a₃ a₄ a₅ (G.degree v) =
      a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) +
        a₅ * (degreeCount G 5 : ℝ) := by
    have hc : ∀ v : Fin n, coeff a₃ a₄ a₅ (G.degree v) =
        (if G.degree v = 3 then a₃ else 0) + (if G.degree v = 4 then a₄ else 0) +
          (if G.degree v = 5 then a₅ else 0) := by
      intro v
      rcases hdeg v with h' | h' | h' <;> simp [coeff, h']
    rw [Finset.sum_congr rfl fun v _ => hc v]
    simp only [Finset.sum_add_distrib, sum_ite_degree_const]
  have hle : ∀ v ∈ (Finset.univ : Finset (Fin n)),
      C v ≤ coeff a₃ a₄ a₅ (G.degree v) -
        transferTerm (G.degree v) (nbrCount G v 3) (nbrCount G v 4) (nbrCount G v 5)
          t₃₄ t₃₅ t₄₅ := by
    intro v _
    linarith [h v]
  have hfinal := Finset.sum_le_sum hle
  rw [Finset.sum_sub_distrib, hcoeff, hsum, sub_zero] at hfinal
  exact hfinal

end T3
end CubicPathwidth

#print axioms CubicPathwidth.T3.charging5