import CubicPathwidth.BoundaryAsymptotics
import CubicPathwidth.CorePruning
import CubicPathwidth.SectionAssembly
import CubicPathwidth.BisectionLimit

/-!
# Boundary transfer from the remaining tree and core-lifting constructions

The induction, graph counting, component concatenation, and uniform limit
are proved here. Two structural construction inputs remain explicit:
finding a narrow tree component, and lifting a path decomposition of the
suppressed simple core. Neither input is asserted as an axiom or theorem.
-/

noncomputable section
namespace CubicPathwidth
open SectionDecomposition

/-- A convenient sublinear allowance. A logarithmic bound is unnecessary
for the original asymptotic statement; this larger allowance simplifies
the future finite construction estimates. -/
def coreOverhead (n : ℕ) : ℝ := 6 * Real.sqrt (n : ℝ) + 6

theorem coreOverhead_nonneg (n : ℕ) : 0 ≤ coreOverhead n := by
  unfold coreOverhead
  positivity

theorem coreOverhead_mono : Monotone coreOverhead := by
  intro m n hmn
  have hmn' : (m : ℝ) ≤ n := by exact_mod_cast hmn
  have hs := Real.sqrt_le_sqrt hmn'
  unfold coreOverhead
  linarith

theorem coreOverhead_sublinear : SublinearError coreOverhead := by
  intro ε hε
  obtain ⟨N, hN⟩ := eventually_sqrt_error 1 (ε / 8) (by linarith)
  obtain ⟨M, hM⟩ := exists_nat_ge (12 / ε)
  refine ⟨max N M, ?_⟩
  intro n hn
  have hs := hN n ((le_max_left N M).trans hn)
  have hm : (M : ℝ) ≤ n := by exact_mod_cast ((le_max_right N M).trans hn)
  have he := (div_le_iff₀ hε).mp (hM.trans hm)
  simp only [mul_one] at hs
  unfold coreOverhead
  nlinarith

/-- Missing tree construction: failure of the component-excess condition
supplies a nonempty closed component with a narrow path decomposition. -/
def ForestComponentBound (L : ℕ → ℝ) : Prop :=
  ∀ n : ℕ, ∀ G : SimpleGraph (Fin n), IsSubcubic G → ∀ F : Finset (Fin n),
    ¬ NonnegativeComponentExcess G F →
      ∃ T : Finset (Fin n), T.Nonempty ∧ T ⊆ F ∧ ClosedIn G F T ∧
        ∃ P : SectionDecomposition G T, P.toBagPath.WidthAtMost (L F.card)

/-- Missing core construction: suppress degree-two paths to a simple graph
on exactly the degree-three core vertices, then lift its decomposition
through subdivisions, cycle components, and pendant trees. -/
def CoreLiftingBound (L : ℕ → ℝ) : Prop :=
  ∀ n : ℕ, ∀ G : SimpleGraph (Fin n), IsSubcubic G → ∀ F C : Finset (Fin n),
    LeafPrunes G F C → (∀ v ∈ C, 2 ≤ (sectionNeighbors G C v).card) →
      ∃ K : SimpleGraph (Fin (C.filter (fun v => (sectionNeighbors G C v).card = 3)).card),
        IsSubcubic K ∧ ∀ p : ℝ, HasPathwidthAtMost K p →
          ∃ P : SectionDecomposition G F, P.toBagPath.WidthAtMost (p + L F.card)

/-- All other finite endpoint steps are checked, conditional on the two
explicit remaining structural constructions. -/
theorem finiteEndpointTransfer_of_tree_and_core {L : ℕ → ℝ}
    (hmono : Monotone L) (hpos : ∀ m, 0 ≤ L m)
    (hforest : ForestComponentBound L) (hcore : CoreLiftingBound L) :
    FiniteEndpointTransfer L := by
  classical
  intro b C hb hb' hC hAffine n G hG X
  have hsections : ∀ U Y : Finset (Fin n), Y ⊆ U →
      HasEndingSection G U Y (endpointBudget b C L U.card Y.card) := by
    apply endingSection_induction G (endpointBudget b C L)
      (fun _ _ _ _ hm hx => endpointBudget_mono hb hb' hmono hm hx)
      (fun m x _ => endpointBudget_ge_size b C hpos m x)
    intro U Y hY hs hrec
    let F := U \ Y
    have hF : F ⊆ U := Finset.sdiff_subset
    have hFc : F.card ≤ U.card := Finset.card_le_card hF
    by_cases hgood : NonnegativeComponentExcess G F
    · obtain ⟨Cores, hp, hmin, hcount⟩ := exists_core_branch_bound G hG hY hs hgood
      obtain ⟨K, hK, hLift⟩ := hcore n G hG F Cores hp hmin
      obtain ⟨P, hP⟩ := hLift _ (hAffine _ K hK)
      have hend := ending_hold P Y hP
      have hunion : F ∪ Y = U := Finset.sdiff_union_of_subset hY
      have hcountR :
          ((Cores.filter (fun v => (sectionNeighbors G Cores v).card = 3)).card : ℝ) +
            3 * (Y.card : ℝ) ≤ (U.card : ℝ) := by exact_mod_cast hcount
      have hmul := mul_le_mul_of_nonneg_left hcountR hb
      have hL := hmono hFc
      have hmax := le_max_right ((Y.card : ℝ) + 1)
        (b * (U.card : ℝ) + (1 - 3 * b) * (Y.card : ℝ) + C)
      have hend' := hend.mono (show
          b * ((Cores.filter (fun v => (sectionNeighbors G Cores v).card = 3)).card : ℝ) +
            C + L F.card + (Y.card : ℝ) ≤ endpointBudget b C L U.card Y.card by
        unfold endpointBudget
        nlinarith)
      simpa only [hunion] using hend'
    · obtain ⟨T, hTne, hTF, hclosed, Q, hQ⟩ := hforest n G hG F hgood
      have hTU : T ⊆ U := hTF.trans hF
      have hYT : Y ⊆ U \ T := by
        intro v hv
        refine Finset.mem_sdiff.mpr ⟨hY hv, ?_⟩
        intro hvT
        exact (Finset.mem_sdiff.mp (hTF hvT)).2 hv
      have hsmall : (U \ T).card < U.card := by
        have hc := Finset.card_sdiff_add_card_eq_card hTU
        have ht := Finset.card_pos.mpr hTne
        omega
      obtain ⟨P, hEnd, hP⟩ := hrec (U \ T) Y hsmall hYT
      have hP' := hP.mono (endpointBudget_mono hb hb' hmono hsmall.le le_rfl)
      have hsep : ∀ v ∈ T, ∀ u ∈ U \ T, G.Adj v u → u ∈ Y := by
        intro v hv u hu hadj
        by_contra huY
        have huF : u ∈ F := Finset.mem_sdiff.mpr ⟨(Finset.mem_sdiff.mp hu).1, huY⟩
        exact (Finset.mem_sdiff.mp hu).2 (hclosed v hv u huF hadj)
      have hend := append_component P Q Y hYT Finset.sdiff_disjoint hEnd hsep hP' hQ
      have hL := hmono hFc
      have hmax := le_max_left ((Y.card : ℝ) + 1)
        (b * (U.card : ℝ) + (1 - 3 * b) * (Y.card : ℝ) + C)
      have hend' := hend.mono (max_le le_rfl (by unfold endpointBudget; linarith))
      simpa only [Finset.sdiff_union_of_subset hTU] using hend'
  obtain ⟨P, hEnd, hP⟩ := hsections Finset.univ X (Finset.subset_univ _)
  refine ⟨P.toFull, hEnd, ?_⟩
  simpa using P.toFull_width hP

/-- Reduction to the two missing constructions for the explicit square-root
overhead. This is NOT an unconditional proof of BoundaryTransferClaim. -/
theorem boundaryTransfer_of_tree_and_core
    (hforest : ForestComponentBound coreOverhead)
    (hcore : CoreLiftingBound coreOverhead) : BoundaryTransferClaim :=
  boundaryTransfer_of_finite coreOverhead_sublinear
    (finiteEndpointTransfer_of_tree_and_core coreOverhead_mono coreOverhead_nonneg hforest hcore)

end CubicPathwidth