CubicPathwidth.Alg.Proofs2.AlgoT4Internal

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

import CubicPathwidth.Alg.Plan2Deletion
import CubicPathwidth.Alg.Proofs.Targets
import CubicPathwidth.T4.SeqH

/-!
# K4b: internal form of Theorem 4 for `algo_T4` (`AlgoT4InternalBound`)

Task `algoT4InternalBound_of` (`Plan2Deletion.lean`, K4b). Hypotheses: `SweepComponentBound`
(K4a), `AlgoT4Width` (A3), `ThinComponentWidth` (U5), `DeletionProcessBound` (D5),
`AlgoT4NoFallback` (N4), `T4FinalFacts`, `PsiPortFacts` (D3), `RelabelOfSimpleGraph` (X1),
`DegreeTransfer` (X3). Taken from Stage 1 / T4: `ofSimpleGraphSpec`, `T4.seqClaim_h`.

Route: the labeler is chosen per graph by `SweepComponentBound` (at `ε/2`). Every bag
of `final` has at most `U0 + 1` vertices, where `U0 = ∑ψ⁻ + σ₃ + (ε/2) n₀ + N₁ + B`,
`B = 3 log₂ n₀ + 1`, `n₀` the number of non-isolated vertices. Then `A3` and `D5` give
`pdWidth ≤ DW + σ₃ + ε n₀ + N₁ + (6 log₂ n₀ + 2)` with `DW = degreeWeight S thm4Coeff`.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace K4b

/-! ## 1. Bag widths -/

theorem maxBagCard_cast_le (bags : List Bag) (w : ℝ) (hw : 0 ≤ w)
    (h : ∀ B ∈ bags, (B.toFinset.card : ℝ) ≤ w) : (maxBagCard bags : ℝ) ≤ w := by
  induction bags with
  | nil => simpa [maxBagCard] using hw
  | cons B bs ih =>
    have h1 : (B.toFinset.card : ℝ) ≤ w := h B (by simp)
    have h2 : (maxBagCard bs : ℝ) ≤ w := ih (fun C hC => h C (by simp [hC]))
    have hc : maxBagCard (B :: bs) = max B.toFinset.card (maxBagCard bs) := by
      simp [maxBagCard]
    rw [hc, Nat.cast_max]
    exact max_le h1 h2

theorem pdWidth_le_of_bags (bags : List Bag) (w : ℝ) (hw : 0 ≤ w + 1)
    (h : ∀ B ∈ bags, (B.toFinset.card : ℝ) ≤ w + 1) : pdWidth bags ≤ w := by
  have := maxBagCard_cast_le bags (w + 1) hw h
  unfold pdWidth
  linarith

theorem card_le_maxBagCard (B : Bag) : ∀ bags : List Bag, B ∈ bags →
    B.toFinset.card ≤ maxBagCard bags := by
  intro bags
  induction bags with
  | nil => intro h; simp at h
  | cons C cs ih =>
    intro h
    have hc : maxBagCard (C :: cs) = max C.toFinset.card (maxBagCard cs) := by
      simp [maxBagCard]
    rw [hc]
    rcases List.mem_cons.1 h with h' | h'
    · subst h'
      exact le_max_left _ _
    · exact le_max_of_le_right (ih h')

theorem card_le_of_pdWidth (bags : List Bag) (w : ℝ) (hp : pdWidth bags ≤ w)
    (B : Bag) (hB : B ∈ bags) : (B.toFinset.card : ℝ) ≤ w + 1 := by
  have h1 : (B.toFinset.card : ℝ) ≤ (maxBagCard bags : ℝ) := by
    exact_mod_cast card_le_maxBagCard B bags hB
  unfold pdWidth at hp
  linarith

/-! ## 2. Sums over `range n` and the potential of `ofSimpleGraph` -/

theorem sum_range_map (n : ℕ) (f : ℕ → ℝ) :
    ((List.range n).map f).sum = ∑ i : Fin n, f i.val := by
  induction n with
  | zero => simp
  | succ m ih =>
    rw [List.range_succ, List.map_append, List.sum_append, ih, Fin.sum_univ_castSucc]
    simp

theorem psiPort_ofSimpleGraph {n : ℕ} (S : SimpleGraph (Fin n)) [DecidableRel S.Adj]
    (hdeg : ∀ i : Fin n, (Graph.ofSimpleGraph S).degree i.val = S.degree i) (b : ℕ → ℝ) :
    psiPort b (Graph.ofSimpleGraph S) = T4.degreeWeight S b := by
  unfold psiPort T4.degreeWeight
  have hn : (Graph.ofSimpleGraph S).nodes = List.range n := rfl
  rw [hn, sum_range_map n (fun v => b ((Graph.ofSimpleGraph S).degree v))]
  apply Finset.sum_congr rfl
  intro i _
  rw [hdeg i]
  convert rfl

theorem nonIsolated_numNodes_eq {n : ℕ} (S : SimpleGraph (Fin n)) [DecidableRel S.Adj]
    (hWF : (Graph.ofSimpleGraph S).WF)
    (hdeg : ∀ i : Fin n, (Graph.ofSimpleGraph S).degree i.val = S.degree i) :
    (nonIsolated (Graph.ofSimpleGraph S)).numNodes = nonIsolatedCount S := by
  have hn : (Graph.ofSimpleGraph S).nodes = List.range n := rfl
  have hnd : (nonIsolated (Graph.ofSimpleGraph S)).nodes.Nodup := by
    unfold nonIsolated
    exact (inducedSpec _ _ hWF).1.nodup
  have hmem : ∀ x, x ∈ (nonIsolated (Graph.ofSimpleGraph S)).nodes ↔
      x < n ∧ (Graph.ofSimpleGraph S).degree x ≠ 0 := by
    intro x
    have h := (inducedSpec (Graph.ofSimpleGraph S)
      (fun v => (Graph.ofSimpleGraph S).degree v != 0) hWF).2.1 x
    unfold nonIsolated
    rw [h, hn, List.mem_range]
    simp
  have hset : (nonIsolated (Graph.ofSimpleGraph S)).nodes.toFinset =
      (Finset.univ.filter fun v : Fin n => S.degree v ≠ 0).map Fin.valEmbedding := by
    ext x
    rw [List.mem_toFinset, Finset.mem_map, hmem]
    constructor
    · rintro ⟨hxn, hxd⟩
      refine ⟨⟨x, hxn⟩, Finset.mem_filter.2 ⟨Finset.mem_univ _, ?_⟩, rfl⟩
      have h := hdeg ⟨x, hxn⟩
      rw [← h]
      exact hxd
    · rintro ⟨i, hi, rfl⟩
      have hi' : S.degree i ≠ 0 := (Finset.mem_filter.1 hi).2
      refine ⟨i.isLt, ?_⟩
      show (Graph.ofSimpleGraph S).degree i.val ≠ 0
      rw [hdeg i]
      exact hi'
  unfold Graph.numNodes nonIsolatedCount
  rw [← List.toFinset_card_of_nodup hnd, hset, Finset.card_map]
  convert rfl

/-! ## 3. A linear bound for `6 log₂ n + 2` -/

theorem log_linear (c η : ℝ) (hc : 0 ≤ c) (hη : 0 < η) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → 3 * (Nat.log 2 n : ℝ) + 1 + c ≤ η * n := by
  have hL : 0 < Real.log 2 := Real.log_pos (by norm_num)
  have hlog : ∀ n : ℕ, 1 ≤ n → (Nat.log 2 n : ℝ) * Real.log 2 ≤ 2 * Real.sqrt n := by
    intro n hn
    have hn0 : (0:ℝ) < n := by exact_mod_cast hn
    have h2 : ((2:ℝ) ^ Nat.log 2 n) ≤ n := by
      exact_mod_cast Nat.pow_log_le_self 2 (by omega)
    have h3 : (Nat.log 2 n : ℝ) * Real.log 2 = Real.log ((2:ℝ) ^ Nat.log 2 n) := by
      rw [Real.log_pow]
    have h4 : Real.log n ≤ 2 * Real.sqrt n := by
      have hs : 0 < Real.sqrt n := Real.sqrt_pos.2 hn0
      have h5 := Real.log_le_sub_one_of_pos hs
      rw [Real.log_sqrt hn0.le] at h5
      linarith
    rw [h3]
    exact (Real.log_le_log (by positivity) h2).trans h4
  set K : ℝ := 6 / Real.log 2 with hK
  have hK0 : 0 ≤ K := by positivity
  set S₀ : ℝ := (K + 1 + c) / η + 1 with hS₀
  have hS₀1 : 1 ≤ S₀ := by
    have : 0 ≤ (K + 1 + c) / η := by positivity
    linarith
  refine ⟨⌈S₀ ^ 2⌉₊ + 1, fun n hn => ?_⟩
  have hn1 : 1 ≤ n := by omega
  have hnS : S₀ ^ 2 ≤ (n : ℝ) := by
    have h : (⌈S₀ ^ 2⌉₊ : ℝ) ≤ n := by
      exact_mod_cast (show ⌈S₀ ^ 2⌉₊ ≤ n by omega)
    exact (Nat.le_ceil _).trans h
  set s : ℝ := Real.sqrt n with hs
  have hs0 : 0 ≤ s := Real.sqrt_nonneg _
  have hsS : S₀ ≤ s := by
    calc S₀ = Real.sqrt (S₀ ^ 2) := (Real.sqrt_sq (by linarith)).symm
      _ ≤ Real.sqrt n := Real.sqrt_le_sqrt hnS
  have hsq : s ^ 2 = (n : ℝ) := Real.sq_sqrt (by positivity)
  have hk : 3 * (Nat.log 2 n : ℝ) ≤ K * s := by
    have h1 : (Nat.log 2 n : ℝ) ≤ 2 * s / Real.log 2 := by
      rw [le_div_iff₀ hL]
      have := hlog n hn1
      linarith
    have h2 : K * s = 6 * s / Real.log 2 := by rw [hK]; ring
    rw [h2]
    calc 3 * (Nat.log 2 n : ℝ) ≤ 3 * (2 * s / Real.log 2) := by linarith
      _ = 6 * s / Real.log 2 := by ring
  have he : η * ((K + 1 + c) / η) = K + 1 + c := by field_simp
  have h1 : K + 1 + c ≤ η * S₀ := by
    have : η * S₀ = η * ((K + 1 + c) / η) + η := by rw [hS₀]; ring
    rw [this, he]
    linarith
  have hA : (K + 1 + c) * s ≤ η * S₀ * s := mul_le_mul_of_nonneg_right h1 hs0
  have hB : η * S₀ * s ≤ η * s * s := by
    apply mul_le_mul_of_nonneg_right _ hs0
    exact mul_le_mul_of_nonneg_left hsS hη.le
  have hC : K * s + 1 + c ≤ (K + 1 + c) * s := by
    nlinarith [mul_nonneg (by linarith : (0:ℝ) ≤ 1 + c) (by linarith : (0:ℝ) ≤ s - 1)]
  calc 3 * (Nat.log 2 n : ℝ) + 1 + c ≤ K * s + 1 + c := by linarith
    _ ≤ η * s * s := by linarith
    _ = η * n := by rw [← hsq]; ring

theorem logBound (ε : ℝ) (hε : 0 < ε) :
    ∃ C : ℝ, ∀ n : ℕ, 6 * (Nat.log 2 n : ℝ) + 2 ≤ ε / 2 * n + C := by
  obtain ⟨N, hN⟩ := log_linear 0 (ε / 4) le_rfl (by linarith)
  have hC0 : (0 : ℝ) ≤ 6 * (Nat.log 2 N : ℝ) + 2 := by positivity
  refine ⟨6 * (Nat.log 2 N : ℝ) + 2, fun n => ?_⟩
  have hn : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
  have hεn : 0 ≤ ε / 2 * (n : ℝ) := by positivity
  by_cases h : N ≤ n
  · have := hN n h
    linarith
  · have hlt : n ≤ N := by omega
    have hlog : Nat.log 2 n ≤ Nat.log 2 N := Nat.log_mono_right hlt
    have hlogR : (Nat.log 2 n : ℝ) ≤ (Nat.log 2 N : ℝ) := by exact_mod_cast hlog
    linarith

end K4b

open K4b

/-! ## 4. The internal bound (main theorem, namespace `CubicPathwidth.Alg`) -/

theorem algoT4InternalBound_of (hSw : SweepComponentBound) (hA3 : AlgoT4Width)
    (hU5 : ThinComponentWidth) (hD5 : DeletionProcessBound) (hN4 : AlgoT4NoFallback)
    (hFin : T4FinalFacts) (hPsi : PsiPortFacts) (hX1 : RelabelOfSimpleGraph)
    (hX3 : DegreeTransfer) : AlgoT4InternalBound := by
  unfold DegreeTransfer at hX3
  have hSeq : T4.BootProps T4.sigma ∧ ∀ d : ℕ, T4.sigma d ≤ T4.thm4Coeff d :=
    T4.seqClaim_h
  have hσ3 : (0 : ℝ) ≤ T4.sigma 3 := by norm_num [T4.sigma]
  intro hT ε hε
  obtain ⟨N₁, hN₁⟩ := hSw hT (ε / 2) (by linarith)
  obtain ⟨C₂, hC₂⟩ := logBound ε hε
  have hN₁0 : (0 : ℝ) ≤ N₁ := Nat.cast_nonneg _
  -- labels: one sweep labeling per graph (chosen with `SweepComponentBound`)
  have hex : ∀ J : Graph, ∃ Y : Labels,
      (J.WF ∧ J.MaxDegLE 5 ∧ ∀ v ∈ J.nodes, 3 ≤ J.degree v) →
        pdWidth (plainLayout J Y) ≤ psiPort T4.sigma J + ε / 2 * (J.numNodes : ℝ) + N₁ := by
    intro J
    by_cases h : J.WF ∧ J.MaxDegLE 5 ∧ ∀ v ∈ J.nodes, 3 ≤ J.degree v
    · obtain ⟨Y, hY⟩ := hN₁ J h.1 h.2.1 h.2.2
      exact ⟨Y, fun _ => hY⟩
    · exact ⟨fun _ => 0, fun h' => absurd h' h⟩
  choose lab hlab using hex
  refine ⟨T4.sigma 3 + N₁ + C₂, ?_⟩
  intro n S _
  have hO : OfSimpleGraphSpec := ofSimpleGraphSpec
  have hWF : (Graph.ofSimpleGraph S).WF := (hO n S).1
  have hrel : IsRelabel (Graph.ofSimpleGraph S) S Fin.val := hX1 n S
  have hdeg : ∀ i : Fin n, (Graph.ofSimpleGraph S).degree i.val = S.degree i := by
    intro i
    have h := hX3 _ n S Fin.val hWF hrel i
    convert h.symm
  have hN : (algoT4Full (Graph.ofSimpleGraph S) lab).fallback = false := hN4 _ hWF lab
  refine ⟨lab, hN, ?_⟩
  have hFe := hFin _ hWF lab hN
  have hDe := hD5 _ hWF lab hN
  have hAe := hA3 _ hWF lab hN
  have hUe := hU5 _ hWF lab hN
  have hcnt := nonIsolated_numNodes_eq S hWF hdeg
  have hPsiG := psiPort_ofSimpleGraph S hdeg T4.sigma
  have hDW : T4.degreeWeight S T4.sigma ≤ T4.degreeWeight S T4.thm4Coeff := by
    unfold T4.degreeWeight
    exact Finset.sum_le_sum fun v _ => hSeq.2 _
  have hPiece : ∀ e ∈ (algoT4Full (Graph.ofSimpleGraph S) lab).final,
      e.graph.WF ∧ e.graph.nodes ≠ [] ∧ ∀ v ∈ e.graph.nodes, 3 ≤ e.graph.degree v := by
    intro e he
    obtain ⟨h1, h2, _, h4⟩ := (hFe e he).1
    exact ⟨h1, h2, h4⟩
  have hnonneg : ∀ e ∈ (algoT4Full (Graph.ofSimpleGraph S) lab).final,
      0 ≤ psiMinusPort T4.sigma e.graph := by
    intro e he
    obtain ⟨h1, h2, h4⟩ := hPiece e he
    exact (hPsi T4.sigma hSeq.1 e.graph h1 h2 h4).1
  have hall : ∀ x ∈ ((algoT4Full (Graph.ofSimpleGraph S) lab).final.map
      fun e => psiMinusPort T4.sigma e.graph), 0 ≤ x := by
    intro x hx
    obtain ⟨e, he, rfl⟩ := List.mem_map.1 hx
    exact hnonneg e he
  have hSg0 : 0 ≤ ((algoT4Full (Graph.ofSimpleGraph S) lab).final.map
      fun e => psiMinusPort T4.sigma e.graph).sum := List.sum_nonneg hall
  have hSgle : ∀ e ∈ (algoT4Full (Graph.ofSimpleGraph S) lab).final,
      psiMinusPort T4.sigma e.graph ≤ ((algoT4Full (Graph.ofSimpleGraph S) lab).final.map
        fun e => psiMinusPort T4.sigma e.graph).sum := by
    intro e he
    apply List.single_le_sum hall
    exact List.mem_map_of_mem he
  obtain ⟨n₀, hn₀⟩ : ∃ m : ℕ, m = (nonIsolated (Graph.ofSimpleGraph S)).numNodes :=
    ⟨_, rfl⟩
  obtain ⟨Sg, hSg⟩ : ∃ s : ℝ, s = ((algoT4Full (Graph.ofSimpleGraph S) lab).final.map
      fun e => psiMinusPort T4.sigma e.graph).sum := ⟨_, rfl⟩
  rw [← hSg] at hSg0 hSgle hDe
  rw [← hn₀] at hAe
  have hB0 : (0 : ℝ) ≤ (Nat.log 2 n₀ : ℝ) := Nat.cast_nonneg _
  have hεn0 : 0 ≤ ε / 2 * (n₀ : ℝ) := mul_nonneg (by linarith) (Nat.cast_nonneg _)
  have hbag : ∀ e ∈ (algoT4Full (Graph.ofSimpleGraph S) lab).final,
      pdWidth (t4Decompose lab e).1 ≤
        Sg + T4.sigma 3 + ε / 2 * (n₀ : ℝ) + N₁ + (3 * (Nat.log 2 n₀ : ℝ) + 1) := by
    intro e he
    have hnum : (e.graph.numNodes : ℝ) ≤ (n₀ : ℝ) := by
      rw [hn₀]
      exact_mod_cast (hFe e he).2.1
    cases hk : e.kind with
    | sweep =>
      have hdeg5 : e.graph.MaxDegLE 5 := (hFe e he).2.2 hk
      have hdec : (t4Decompose lab e).1 = plainLayout e.graph (lab e.graph) := by
        simp [t4Decompose, hk]
      rw [hdec]
      obtain ⟨hw, hne, hmin⟩ := hPiece e he
      have h1 := hlab e.graph ⟨hw, hdeg5, hmin⟩
      have h2 := (hPsi T4.sigma hSeq.1 e.graph hw hne hmin).2
      have h3 := hSgle e he
      have h4 : ε / 2 * (e.graph.numNodes : ℝ) ≤ ε / 2 * (n₀ : ℝ) :=
        mul_le_mul_of_nonneg_left hnum (by linarith)
      linarith
    | thin =>
      have hU := hUe e he hk
      have hlog : Nat.log 2 e.graph.numNodes ≤ Nat.log 2 n₀ := by
        rw [hn₀]
        exact Nat.log_mono_right (hFe e he).2.1
      have hlogR : (Nat.log 2 e.graph.numNodes : ℝ) ≤ (Nat.log 2 n₀ : ℝ) := by
        exact_mod_cast hlog
      linarith
  have hU0 : 0 ≤ Sg + T4.sigma 3 + ε / 2 * (n₀ : ℝ) + N₁ + (3 * (Nat.log 2 n₀ : ℝ) + 1) := by
    linarith
  have hflat : pdWidth (((algoT4Full (Graph.ofSimpleGraph S) lab).final.map
        (t4Decompose lab)).flatMap (·.1)) ≤
      Sg + T4.sigma 3 + ε / 2 * (n₀ : ℝ) + N₁ + (3 * (Nat.log 2 n₀ : ℝ) + 1) := by
    refine pdWidth_le_of_bags _ _ (by linarith) ?_
    intro B hB
    obtain ⟨part, hpart, hBp⟩ := List.mem_flatMap.1 hB
    obtain ⟨e, he, rfl⟩ := List.mem_map.1 hpart
    exact card_le_of_pdWidth _ _ (hbag e he) B hBp
  have hεcount : ε * (n₀ : ℝ) = ε * (nonIsolatedCount S : ℝ) := by
    rw [hn₀, hcnt]
  have hlogn := hC₂ n₀
  linarith

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.algoT4InternalBound_of