Pebbling number conjecture

Reference: Wikipedia

def PebbleDistribution (V : Type) : Type

A Pebble distribution is an assigment of zero or more pebbles to each of the vertices.

Equations

• PebbleDistribution V = (V → ℕ)

def NumberOfPebbles {V : Type} [Fintype V] : PebbleDistribution V → ℕ

The number of pebbles of a distribution is the total number summed over all vertices.

Equations

• NumberOfPebbles D = ∑ v : V, D v

def IsPebblingMove {V : Type} [DecidableEq V] (G : SimpleGraph V) (A B : PebbleDistribution V) : Prop

A pebbling move on a graph consists of choosing a vertex with at least two pebbles, removing two pebbles from it, and adding one to an adjacent vertex (the second removed pebble is discarded from play).

Equations

• IsPebblingMove G A B = ∃ (v : V) (w : V), A v ≥ 2 ∧ G.Adj v w ∧ B = fun (u : V) => if u = w then A u + 1 else if u = v then A u - 2 else A u

inductive PebblePath {α : Type} (r : α → α → Prop) : α → α → Type

A pebble path is a series of pebbling moves.

• refl {α : Type} {r : α → α → Prop} (a : α) : PebblePath r a a
• step {α : Type} {r : α → α → Prop} {a b c : α} (p : PebblePath r a b) (h : r b c) : PebblePath r a c

def ExistsPebblePath {α : Type} (r : α → α → Prop) (a b : α) : Prop

Indicates whether there exists a sequence of pebbling moves transforming one pebble distribution to another.

Equations

• ExistsPebblePath r a b = Nonempty (PebblePath r a b)

def IsReachable {V : Type} [DecidableEq V] (G : SimpleGraph V) (A B : PebbleDistribution V) : Prop

A pebble distribution B is reachable from another pebble distribution A, if there exists a sequence of pebbling moves transforming the first into the second.

Equations

• IsReachable G A B = ExistsPebblePath (IsPebblingMove G) A B

noncomputable def PebblingNumber {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : ℕ

The pebbling number of a graph G, is the lowest natural number n that satisfies the following condition: Given any target or 'root' vertex in the graph and any initial pebbles distribution with n pebbles on the graph, another pebble distribution is reachable in which the designated root vertex has one or more pebbles.

Equations

• PebblingNumber G = sInf {n : ℕ | ∀ (D : PebbleDistribution V), NumberOfPebbles D = n → ∀ (v : V), ∃ (D' : PebbleDistribution V), IsReachable G D D' ∧ 1 ≤ D' v}

theorem PebblingNumber_completeGraph {V : Type} [Fintype V] [DecidableEq V] : PebblingNumber (completeGraph V) = Fintype.card V

The pebbling number of the complete graph on n vertices is n.

theorem pebbling_number_conjecture {V : Type} [Fintype V] [DecidableEq V] (G H : SimpleGraph V) : PebblingNumber (G □ H) ≤ PebblingNumber G * PebblingNumber H

The pebbling number conjecture: the pebbling number of a Cartesian product of graphs is at most equal to the product of the pebbling numbers of the factors.