CubicPathwidth.Alg.Proofs2.SweepBound

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

import CubicPathwidth.Alg.Plan2Deletion
import CubicPathwidth.T2.HetStar
import CubicPathwidth.T2.StarBoundCont
import CubicPathwidth.T3.Charging5
import CubicPathwidth.T3.DegreeLabels5
import CubicPathwidth.T3.PhiTail5
import CubicPathwidth.T3.Targets
import CubicPathwidth.T4.Assembly

/-!
# Stage 2 task K4a: plain sweep of a component of maximum degree 5

`sweepComponentBound_of : SweepComponentBound` (`Plan2Deletion.lean`, K4a).

Route. Fix the triple `S = (5/32, 1/4, 11/32)` (admissible by hypothesis).
* `T3.goodLabelsCount5_step` with the Stage 1-free existing results `T3.degreeLabels5`,
  `T2.hetStar`, `T2.starBoundCont`, `T3.charging5` and the tail bound `T3.tail_S`
  gives `T3.GoodLabelsCount5` for the triple, hence the threshold `N`.
* For a component `J` (`WF`, degrees in `[3, 5]`), `RelabelExists` gives a simple graph
  `S'` on `Fin J.numNodes` with `IsRelabel J S' e`; `DegreeTransfer` gives the degrees.
* `psiPort sigma J = degreeWeight S' sigma = 5/32 d₃ + 1/4 d₄ + 11/32 d₅`
  (`T4.degreeWeight_sigma_of_maxDeg5`).
* If `N ≤ |J|`: `LabelTransfer` turns the good labels of `S'` into labels `Y` of `J`
  whose outer frontiers are those of `S'`; `PlainLayoutWidth` gives the width bound.
* If `|J| < N`: any injective labeling works; every outer frontier has at most `|J| < N`
  nodes, so the width is at most `N`, and `psiPort sigma J ≥ 0`, `ε |J| ≥ 0`.
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

namespace K4a

/-- `psiPort` is the sum over a relabelling of `J` (the nodes of `J` are the values of `e`,
which is injective). -/
theorem psi_eq_relabel (J : Graph) (hJ : J.WF) {m : ℕ} (S : SimpleGraph (Fin m))
    (e : Fin m → Nat) (hI : IsRelabel J S e) (b : ℕ → ℝ) :
    psiPort b J = ∑ i : Fin m, b (J.degree (e i)) := by
  classical
  have hset : J.nodes.toFinset = Finset.univ.image e := by
    ext v
    simp only [List.mem_toFinset, Finset.mem_image, Finset.mem_univ, true_and]
    exact hI.2.1 v
  unfold psiPort
  rw [← List.sum_toFinset (fun v => b (J.degree v)) hJ.nodup, hset,
    Finset.sum_image (fun x _ y _ h => hI.1 h)]

end K4a

open K4a in

/-- (K4a) Plain sweep of one `.sweep` component with good labels. -/
theorem sweepComponentBound_of (hL2 : PlainLayoutWidth) (hX2 : RelabelExists)
    (hX3 : DegreeTransfer) (hX4 : LabelTransfer) : SweepComponentBound := by
  classical
  unfold SweepComponentBound
  intro hadm ε hε
  have hstep := CubicPathwidth.T3.goodLabelsCount5_step CubicPathwidth.T3.degreeLabels5
    CubicPathwidth.T2.hetStar CubicPathwidth.T2.starBoundCont CubicPathwidth.T3.charging5
    (5 / 32) (1 / 4) (11 / 32) hadm CubicPathwidth.T3.tail_S (by norm_num) (by norm_num)
  obtain ⟨N, hN⟩ := hstep ε hε
  refine ⟨N, fun J hJ hmax hmin => ?_⟩
  obtain ⟨S, e, hI⟩ := hX2 J hJ
  have hdeg : ∀ i, S.degree i = J.degree (e i) := fun i => hX3 J _ S e hJ hI i
  have hemem : ∀ i, e i ∈ J.nodes := fun i => (hI.2.1 (e i)).2 ⟨i, rfl⟩
  have hmaxS : CubicPathwidth.T2.MaxDegreeAtMost 5 S := by
    intro i
    rw [hdeg i]
    exact hmax _ (hemem i)
  have hminS : CubicPathwidth.T2.MinDegreeAtLeast 3 S := by
    intro i
    rw [hdeg i]
    exact hmin _ (hemem i)
  have hpsi : psiPort CubicPathwidth.T4.sigma J =
      (5 / 32) * (CubicPathwidth.T2.degreeCount S 3 : ℝ) +
        (1 / 4) * (CubicPathwidth.T2.degreeCount S 4 : ℝ) +
        (11 / 32) * (CubicPathwidth.T2.degreeCount S 5 : ℝ) := by
    rw [psi_eq_relabel J hJ S e hI CubicPathwidth.T4.sigma,
      ← CubicPathwidth.T4.degreeWeight_sigma_of_maxDeg5 S hmaxS]
    unfold CubicPathwidth.T4.degreeWeight
    exact Finset.sum_congr rfl fun i _ => by rw [hdeg i]
  have hpsi0 : 0 ≤ psiPort CubicPathwidth.T4.sigma J := by
    rw [hpsi]
    positivity
  have h0 : (0 : ℝ) ≤ N := Nat.cast_nonneg N
  by_cases hm : N ≤ J.numNodes
  · obtain ⟨y, hyinj, hyfr⟩ := hN J.numNodes hm S hminS hmaxS
    obtain ⟨Y, hYinj, -, hYout, -, -⟩ := hX4 J _ S e hJ hI y hyinj
    have hbd : ∀ t : ℚ, ((outerFr J Y t).length : ℝ) ≤
        psiPort CubicPathwidth.T4.sigma J + ε * (J.numNodes : ℝ) := by
      intro t
      obtain ⟨s, -, hs⟩ := hYout t
      rw [hs, hpsi]
      exact hyfr s
    have hw := hL2 J hJ Y hYinj _ hbd
    refine ⟨Y, ?_⟩
    linarith
  · push Not at hm
    have hinj : Function.Injective (fun i : Fin J.numNodes => ((i : ℕ) : ℝ)) := by
      intro i j h
      have h' : ((i : ℕ) : ℝ) = ((j : ℕ) : ℝ) := h
      exact Fin.ext (by exact_mod_cast h')
    obtain ⟨Y, hYinj, -⟩ := hX4 J _ S e hJ hI _ hinj
    have hbd : ∀ t : ℚ, ((outerFr J Y t).length : ℝ) ≤ (N : ℝ) := by
      intro t
      have h1 : (outerFr J Y t).length ≤ J.numNodes := List.length_filter_le _ _
      have h2 : (J.numNodes : ℝ) ≤ N := by exact_mod_cast hm.le
      have h3 : ((outerFr J Y t).length : ℝ) ≤ (J.numNodes : ℝ) := by exact_mod_cast h1
      linarith
    have hw := hL2 J hJ Y hYinj _ hbd
    have h1 : (0 : ℝ) ≤ ε * (J.numNodes : ℝ) := by positivity
    refine ⟨Y, ?_⟩
    linarith

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.sweepComponentBound_of
Back to top