import CubicPathwidth.T4.ProcessDefs

/-!
# Proof of the bootstrap lemma from its three children

`bootstrap_of_children : StateClaim → BasicClaim → DeletionClaim → BootstrapClaim`
follows the proof of `lem:bootstrap`:

1. reduce `G` maximally: a state `(univ, B₀)` with torso minimum degree at least `3`
   and `ψ(univ, B₀) ≤ ψ(G) = ∑_v b(d(v))` (`TorsoDynamics`, part 3);
2. run the deletion process (`DeletionClaim`) to a state `(F₁, B₁)` all of whose torso
   components are basic, with `|univ \ F₁| + ψ⁻(F₁, B₁) ≤ ψ⁻(univ, B₀) ≤ ψ(univ, B₀)`;
3. bound the final torso by `max (ψ⁻ + b₃ + (ε/2) n + N₀) (12 √n + 1)`
   (`ComponentClaim` with `KindTwoClaim` for the basic components of the second kind);
4. lift once (`LiftClaim`): `pw(G) ≤ |univ \ F₁| + pw(torso) + 12 √n + 1`;
5. absorb `b₃ + N₀ + 24 √n + 2` into `(ε/2) n` for large `n`.
-/

noncomputable section

namespace CubicPathwidth
namespace T4

open T2 SectionDecomposition

theorem bootstrap_of_children (h2 : StateClaim) (h3 : BasicClaim) (h4 : DeletionClaim) :
    BootstrapClaim := by
  obtain ⟨hdyn, hlift, hkind2⟩ := h2
  obtain ⟨hpsi, hcomp⟩ := h3
  intro b hb hbase ε hε
  obtain ⟨N₀, hN₀⟩ := hcomp b hb hbase (ε / 2) (by linarith)
  obtain ⟨N₂, hN₂⟩ := coreOverhead_sublinear (ε / 16) (by linarith)
  obtain ⟨M, hM⟩ := exists_nat_ge (4 * ((N₀ : ℝ) + 3) / ε)
  refine ⟨max N₂ M, ?_⟩
  intro n hn G
  -- Step 1: maximal reduction of `G`.
  have hgood0 := good_univ G
  obtain ⟨-, -, B₀, hB₀sub, hR₀, hB₀min, hB₀deg⟩ :=
    hdyn n G Finset.univ Finset.univ hgood0
  have hgoodB₀ : Good G Finset.univ B₀ := hgood0.reach hR₀
  have hpsi0 : psi b G Finset.univ B₀ ≤ degreeWeight G b := by
    rw [← psi_univ b G]
    exact psi_le_psi hb hB₀sub hB₀deg
  -- Step 2: the deletion process.
  obtain ⟨F₁, B₁, hR₁, hmin₁, hbasic₁, hpot⟩ :=
    h4 hdyn b hb n G Finset.univ B₀ hgoodB₀ hB₀min
  have hR₀₁ : Reach G (Finset.univ, Finset.univ) (F₁, B₁) := hR₀.trans hR₁
  have hgood₁ : Good G F₁ B₁ := hR₀₁
  have hψ₀ := (hpsi b hb n G Finset.univ B₀ hB₀min).2
  have hψ₁ := (hpsi b hb n G F₁ B₁ hmin₁).1
  -- Step 3: the final torso.
  have hq : ∀ C ∈ tcomps G F₁ B₁, (∀ v ∈ C, tdeg G F₁ B₁ v ≤ 5) ∨
      HasPathwidthAtMost (coreTorso G (F₁ \ (B₁ \ C)) C) (12 * Real.sqrt (n : ℝ) + 1) := by
    intro C hC
    rcases hbasic₁ C hC with h | ⟨v, hv, B'', hR, hdisj⟩
    · exact Or.inl h
    · exact Or.inr (hkind2 n G F₁ B₁ C B'' v hgood₁ hC hv hR hdisj)
  have htorso := hN₀ n G F₁ B₁ hgood₁ hmin₁ _ hq
  -- Step 4: lift once.
  have hlifted := hasPathwidth_of_coreTorso_univ G
    (hlift n G Finset.univ Finset.univ F₁ B₁ _ hgood0 hR₀₁ htorso)
  -- Step 5: arithmetic.
  apply hlifted.mono
  have hsq : 0 ≤ Real.sqrt (n : ℝ) := Real.sqrt_nonneg _
  have hn0 : (0 : ℝ) ≤ n := Nat.cast_nonneg n
  have hb3 : 0 ≤ b 3 := hb.nonneg 3
  have hb3' : b 3 ≤ 1 := hb.le_one 3
  have hmax : max (psiMinus b G F₁ B₁ + b 3 + ε / 2 * n + N₀) (12 * Real.sqrt n + 1) ≤
      psiMinus b G F₁ B₁ + b 3 + ε / 2 * n + N₀ + (12 * Real.sqrt n + 1) := by
    apply max_le
    · linarith
    · have : (0 : ℝ) ≤ N₀ := Nat.cast_nonneg _
      have : 0 ≤ ε / 2 * (n : ℝ) := by positivity
      linarith
  have h1 := hN₂ n ((le_max_left _ _).trans hn)
  unfold coreOverhead at h1
  have hMn : (M : ℝ) ≤ n := by exact_mod_cast (le_max_right _ _).trans hn
  have h2' : 4 * ((N₀ : ℝ) + 3) ≤ ε * n := by
    have := hM.trans hMn
    rw [div_le_iff₀ hε] at this
    linarith
  linarith

end T4
end CubicPathwidth

#print axioms CubicPathwidth.T4.bootstrap_of_children