import CubicPathwidth.T4.Defs
import CubicPathwidth.T3.Targets

/-!
# Parent assembly for Theorem 4 and Corollary 5

Conditional on `SeqClaim`, `BootstrapClaim` and `Cor5Claim`; uses `T3.target3S`.
-/

noncomputable section

namespace CubicPathwidth
namespace T4

open T2 T3

/-- For maximum degree 5, the vertex sum with `sigma` is the degree-count sum. -/
theorem degreeWeight_sigma_of_maxDeg5 {n : ℕ} (G : SimpleGraph (Fin n))
    (h5 : MaxDegreeAtMost 5 G) :
    degreeWeight G sigma =
      (5 / 32) * (degreeCount G 3 : ℝ) + (1 / 4) * (degreeCount G 4 : ℝ) +
        (11 / 32) * (degreeCount G 5 : ℝ) := by
  classical
  unfold degreeWeight degreeCount
  unfold MaxDegreeAtMost at h5
  have key : ∀ v : Fin n, sigma (G.degree v) =
      (5 / 32) * (if G.degree v = 3 then 1 else 0) + (1 / 4) * (if G.degree v = 4 then 1 else 0)
        + (11 / 32) * (if G.degree v = 5 then 1 else 0) := by
    intro v
    have hv := h5 v
    interval_cases h : G.degree v <;> simp [sigma] <;> norm_num
  rw [Finset.sum_congr rfl fun v _ => key v]
  simp only [Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_boole]

theorem theorem4_of_children (hseq : SeqClaim) (hboot : BootstrapClaim)
    (h3 : UniformDegreeCountBound5 (5 / 32) (1 / 4) (11 / 32)) : Theorem4 := by
  have hb := hboot sigma hseq.1 (by
    intro ε hε
    obtain ⟨N, hN⟩ := h3 ε hε
    refine ⟨N, fun n hn G h5 => ?_⟩
    rw [degreeWeight_sigma_of_maxDeg5 G h5]
    exact hN n hn G h5)
  intro ε hε
  obtain ⟨N, hN⟩ := hb ε hε
  refine ⟨N, fun n hn G => ?_⟩
  obtain ⟨D, hD⟩ := hN n hn G
  refine ⟨D, fun i => (hD i).trans ?_⟩
  have : degreeWeight G sigma ≤ degreeWeight G thm4Coeff := by
    classical
    unfold degreeWeight
    exact Finset.sum_le_sum fun v _ => hseq.2 _
  linarith

theorem target4_of_children (hseq : SeqClaim) (hboot : BootstrapClaim) : Target4 :=
  fun hadm => theorem4_of_children hseq hboot (target3S hadm)

theorem target5_of_children (hseq : SeqClaim) (hboot : BootstrapClaim) (hcor : Cor5Claim) :
    Target5 :=
  fun hadm => hcor (target4_of_children hseq hboot hadm)

end T4
end CubicPathwidth

#print axioms CubicPathwidth.T4.target4_of_children
#print axioms CubicPathwidth.T4.target5_of_children