Prove that the Burning Conjecture is true for Path Graphs.
for every connected graph G of order n
— Bonato, Janssen, Roshanbin (AAAI 2016)
An ordered list of vertices s₁,…,sk. At round i: si is set on fire (new source), and every already-burning vertex spreads to its neighbors. Graph is fully burnt when all vertices are burning.
The minimum length of a burning sequence for G. Equivalently: the minimum k such that k rounds suffice to burn all of G.
b(singleton) = 1 · b(P9) = 3
For any connected G of order n. Proven for path graphs by Bonato et al. (2016). This project formalizes that proof.
For every path graph Pn in Isabelle/HOL: ∃ burning sequence of length ≤ ⌈√(card V)⌉
= gap between k² and (k−1)²
= max coverage per source on a path
= exactly the coverage needed
Path graphs are the "most spread-out" structure for given n. Tight bound: b(Pn) = ⌈√n⌉ exactly. Proving bound is tight is future work; this project proves ≤.
Chelsea Edmonds. Undirected Graph Theory, AFP 2022. 7 theory files included locally.
Provides: fin_connected_sgraph, shortest_path, connecting_walk, connecting_walk_split.
definition finite_enumeration :: "('a ⇒ nat) ⇒ 'a set ⇒ bool"
"finite_enumeration f D ≡
(∀d1 d2. f d1 = f d2 → d1 = d2) ∧
(∃m. (∀n<m. ∃d∈D. f d = n) ∧
(∀d∈D. f d < m))"
No library function found. Developed from first principles (Prof. Gunter). The surjectivity clause forces image = {0,…,m−1} exactly — enumeration always starts at 0.
Used in path_graph to index vertices 0..n−1.
closed_nbh k v ≡
{u ∈ V |
shortest_path v u ≤ enat k}
The closed k-ball around v. Source xs[i] ignited at step i has radius |xs|−i−1 remaining rounds.
burns_with xs ≡
xs ≠ [] ∧
set xs ⊆ V ∧
(∀u∈V. ∃i<|xs|.
u ∈ closed_nbh
(|xs|−Suc i) (xs!i))
xs is a valid burning sequence: non-empty, sources in V, every vertex covered within radius budget.
burnable ≡
∃ xs.
burns_with xs ∧
length xs ≤
nat ⌈sqrt (real (card V))⌉
The conjecture for this graph. There exists a valid burning sequence respecting the ⌈√n⌉ bound.
Strategy: construct explicit path_bs, prove burns_with path_bs directly, bound its length → burnable. No searching required.
{u, v} ∈ E ↔
f v = Suc (f u) ∨
f u = Suc (f v)
Vertices u and v are adjacent iff their labels differ by 1. This captures the linear chain structure: each vertex connects only to its immediate label neighbors.
The size parameter used throughout all proofs. Avoids confusion with card V in locale context.
path_dist i j ≡ |i − j|
Absolute difference of two labels, defined outside the locale. Key bound: for i ≤ j < path_length, the walk g(i)→…→g(j) has length exactly j−i, so shortest_path(g i, g j) ≤ path_dist i j.
All four are one-line consequences of locale assumptions. Together they make f and g a verified bijection between V and {0..path_length−1}.
Degree-based definitions are hard to use in distance proofs. Label-based path_adj directly gives path_dist as an upper bound on shortest-path distance — enabling all arithmetic coverage proofs to transfer to graph distances via label_to_closed_nbh.
Prove coverage at the label level first (arithmetic on nats), then lift to graph distances using path_dist ≤ shortest_path.
-- number of sources (recursive depth) path_k ≡ nat ⌈sqrt (real path_length)⌉ -- label list, back-to-front, recursive path_bs_labels (Suc k) = min (k * Suc k) (path_length - 1) # path_bs_labels k -- vertex sequence (the witness) path_bs ≡ map g (path_bs_labels path_k)
Key lemma path_bs_labels_nth_closed: the i-th label is
The min cap at n−1 only activates in the non-square case when i=0's ideal position overshoots the path.
path_bs = [g(6), g(2), g(0)] — sources placed back-to-front to cover intervals [(k-1-i)², (k-i)²).
Conditions 1 and 2 are structural. Condition 3 is the hard part: every vertex v ∈ V must be covered by some source within its radius budget. This requires connecting label arithmetic to graph distances.
burns_with needs graph distances (shortest_path in enat). All our arithmetic works on labels (nat). We need a bridge lemma chain: label arithmetic → graph membership.
i ≤ j < n → connecting_walk(g i)(g j)(map g [i..j])
i,j < n → shortest_path(g i, g j) ≤ enat(|i−j|)
Extracts a path from the walk (AFP: connecting_walk_path), then bounds the shortest path via the path length = j−i.
lemma label_to_closed_nbh: assumes "v ∈ V" assumes "j < path_length" assumes "path_dist (f v) j ≤ r" shows "v ∈ closed_nbh r (g j)"
label_to_closed_nbh is the last step in every coverage argument. All that remains: arithmetic coverage proofs per case.(k−1−i)²≤p<(k−i)² → path_dist p (label i) ≤ k−Suc i
k²≤n, p<k² → ∃i<k. (k−1−i)²≤p<(k−i)²
p < k² → ∃i<k. path_dist p (path_bs_labels k ! i) ≤ k−1−i
Central arithmetic result that feeds directly into perfect_sq_path_burns.
¬sq → (k−1)² < n < k²
From ceiling: k−1 < √n ≤ k. Squaring: previous square = (k−1)², next = k².
r²≤p<(r+1)² → path_dist p (r(r+1)) ≤ r
Source r(r+1) sits at offset r from r²; both halves ≤ r. Case split p ≤ source vs p > source.
f v ∈ [(k−1)², n) → label distance ≤ k−1
Two sub-cases:
(a) Uncapped (n > (k−1)k): source at (k−1)k, use path_dist_source_cover with r=k−1
(b) Capped (n ≤ (k−1)k): source at n−1, tail shorter → distance ≤ k−2
f v < (k−1)² → label distance ≤ k−Suc(Suc j)
Reuse square_interval_partition_upto for k−1 intervals covering [0,(k−1)²). Sources 1..k−1 are always uncapped (nonsquare_source_uncapped). Shift index by 1.
Combines coverage (path_bs_covers_nonsq) with structural lemmas (path_bs_ne, path_bs_in_V) to discharge all three conditions of burns_with. Analogous structure to perfect_sq_path_burns.
non_perfect_sq_path_burns and perfect_sq_path_burns, all path graphs are covered. Exhaustive by case split on is_perfect_square path_length.v∈V → ∃i<path_k. v ∈ closed_nbh(path_k−Suc i)(path_bs!i)
length path_bs = path_k -- path_bs_length = nat ⌈√path_length⌉ -- path_k_def = nat ⌈√(card V)⌉ -- path_length_def ≤ nat ⌈√(card V)⌉ -- hbound
Combine path_burns_with + hbound, unfold burnable → done ✓
burnable holds for every path graph. b(Pn) ≤ ⌈√n⌉ formally verified in Isabelle/HOL. No sorry's. All Isar-style.The constructive proof of Bonato et al. (AAAI 2016) — placing sources at (k−1−i)(k−i) to cover intervals [(k−1−i)², (k−i)²) — is now a machine-checked theorem in Isabelle/HOL.
Prof. Elsa Gunter (UIUC) — guidance on Isabelle/HOL and formalization strategy throughout. Chelsea Edmonds — AFP Undirected Graph Theory library.
Slide visuals, layout, step animations, and the burning graph animation — designed with Claude (Anthropic).
Formalizing Graph Burning for Path Graphs in Isabelle/HOL
theorem path_burnable: "burnable" — for every path graph Pn