import CubicPathwidth.Alg.Plan2
import CubicPathwidth.Alg.Proofs.Targets
import CubicPathwidth.C3.Constants
import CubicPathwidth.C3.GoodLabels
import CubicPathwidth.C3.StarFrontier
import CubicPathwidth.C3.Switch

/-!
# K1: Theorem 1 is realized by `algo_T1`

Task K1 of the formalisation. Conditional on the width bridge `AlgoT1Width`,
the no-fallback statement `AlgoT1NoFallback`, the relabelling `RelabelOfSimpleGraph` and
the label transfer `LabelTransfer`. The good labels at a fixed radius `R ≥ 2` come from the
proved C3 chain `C3.Labels.goodLabels_of_claims C3.starFrontier C3.switchClaim`, the radius
limit from `C3.kappaLimit`, and validity from Stage 1 (`algoT1Exported`, which also uses
`ofSimpleGraphSpec` for well-formedness and the degree bound).

Mirror of `C3.radiusBound_of_children` and `C3.c3MainClaim_of_children`
(`CubicPathwidth/C3/Assembly.lean`).
-/

noncomputable section

namespace CubicPathwidth.Alg

open Graph

theorem algoT1RealizesTheorem1_of (hW : AlgoT1Width) (hN : AlgoT1NoFallback)
    (hX1 : RelabelOfSimpleGraph) (hX4 : LabelTransfer) : AlgoT1RealizesTheorem1 := by
  intro ε hε
  -- a fixed radius `R ≥ 2` whose coefficient is within `ε/2` of `c3`
  have hev : ∀ᶠ R : ℕ in Filter.atTop,
      C3.kappa (C3.radiusCorr R) < C3.c3 + ε / 2 ∧ 2 ≤ R :=
    (C3.kappaLimit.eventually (gt_mem_nhds (by linarith))).and (Filter.eventually_ge_atTop 2)
  obtain ⟨R, hRlt, hR⟩ := hev.exists
  -- good labels at that radius, with slack `ε/4`
  obtain ⟨N₁, hN₁⟩ :=
    C3.Labels.goodLabels_of_claims C3.starFrontier C3.switchClaim R hR (ε / 4) (by linarith)
  refine ⟨max N₁ ⌈4 / ε⌉₊, ?_⟩
  intro n hn S inst hsub
  have hnN₁ : N₁ ≤ n := le_trans (le_max_left _ _) hn
  have hceil : ⌈4 / ε⌉₊ ≤ n := le_trans (le_max_right _ _) hn
  have hn4 : 4 / ε ≤ (n : ℝ) := le_trans (Nat.le_ceil _) (by exact_mod_cast hceil)
  have hεn : 4 ≤ (n : ℝ) * ε := (div_le_iff₀ hε).mp hn4
  have hnn : (0 : ℝ) ≤ n := Nat.cast_nonneg n
  obtain ⟨hWF, -, -, hdeg⟩ := ofSimpleGraphSpec n S
  obtain ⟨y, hy, hin, hout, hlo, hup⟩ := hN₁ n hnN₁ S hsub
  obtain ⟨Y, hYinj, hYnz, hYout, hYin, hYlo, hYup⟩ :=
    hX4 (Graph.ofSimpleGraph S) n S Fin.val hWF (hX1 n S) y hy
  -- numerical room: the frontier bound `(κ + ε/4) n` leaves `1` below `(c3 + ε) n`
  have hbig : (C3.kappa (C3.radiusCorr R) + ε / 4) * n + 1 ≤ (C3.c3 + ε) * n := by
    nlinarith [mul_le_mul_of_nonneg_right hRlt.le hnn]
  -- inner frontiers below zero (the level `s = 0` is bounded by `lowerZero`)
  have hinner : ∀ t : ℚ, t < 0 →
      ((innerFr (Graph.ofSimpleGraph S) Y t).length : ℝ) ≤ (C3.c3 + ε) * n := by
    intro t ht
    obtain ⟨s, hs0, hcard⟩ := hYin t ht
    rw [hcard]
    rcases lt_or_eq_of_le hs0 with hlt | heq
    · have h1 := hin s hlt
      linarith [hbig]
    · subst heq
      have hle : (C3.innerFrontier S y 0).card ≤ C3.lowerZero S y := by
        unfold C3.lowerZero
        omega
      have hle' : ((C3.innerFrontier S y 0).card : ℝ) ≤ ((C3.lowerZero S y : ℕ) : ℝ) := by
        exact_mod_cast hle
      linarith [hbig, hlo]
  -- outer frontiers above zero
  have houter : ∀ t : ℚ, 0 < t →
      ((outerFr (Graph.ofSimpleGraph S) Y t).length : ℝ) ≤ (C3.c3 + ε) * n := by
    intro t ht
    obtain ⟨s, hs0, hcard⟩ := hYout t
    rw [hcard]
    have h1 := hout s (hs0 ht)
    linarith [hbig]
  -- the connector level: `max(L₀, L₀') + 1`
  have hmax : max ((lowerZeroP (Graph.ofSimpleGraph S) Y : ℕ) : ℝ)
      ((upperZeroP (Graph.ofSimpleGraph S) Y : ℕ) : ℝ) + 1 ≤ (C3.c3 + ε) * n := by
    rw [hYlo, hYup]
    have h3 := max_le hlo hup
    linarith [hbig, h3]
  have hWidth : pdWidth (algoT1 (Graph.ofSimpleGraph S) Y) ≤ (C3.c3 + ε) * n :=
    hW (Graph.ofSimpleGraph S) hWF (hdeg hsub) Y hYinj hYnz ((C3.c3 + ε) * n) hinner houter
      hmax
  refine ⟨Y, ?_, algoT1Exported n S hsub Y, hWidth⟩
  exact hN (Graph.ofSimpleGraph S) hWF (hdeg hsub) Y

end CubicPathwidth.Alg

#print axioms CubicPathwidth.Alg.algoT1RealizesTheorem1_of