Pebbling number conjecture

Reference: Wikipedia

def PebblingNumberConjecture.PebbleDistribution (V : Type) : Type

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

Equations

• PebblingNumberConjecture.PebbleDistribution V = (V → ℕ)

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

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

Equations

• PebblingNumberConjecture.NumberOfPebbles D = ∑ v : V, D v

def PebblingNumberConjecture.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

• PebblingNumberConjecture.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

theorem PebblingNumberConjecture.IsPebblingMove.refl {V : Type} [DecidableEq V] (G : SimpleGraph V) (A : PebbleDistribution V) {v w : V} (hv : 2 ≤ A v) (hvw : G.Adj v w) : IsPebblingMove G A fun (u : V) => if u = w then A u + 1 else if u = v then A u - 2 else A u

inductive PebblingNumberConjecture.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 PebblingNumberConjecture.ExistsPebblePath {α : Type} (r : α → α → Prop) (a b : α) : Prop

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

Equations

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

def PebblingNumberConjecture.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

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

@[simp]

theorem PebblingNumberConjecture.IsReachable.refl {V : Type} [DecidableEq V] (G : SimpleGraph V) (A : PebbleDistribution V) : IsReachable G A A

noncomputable def PebblingNumberConjecture.PebblingNumber {V : Type} [DecidableEq V] [Fintype 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

• One or more equations did not get rendered due to their size.

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

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

theorem PebblingNumberConjecture.pebbling_number_conjecture {V : Type} [DecidableEq V] [Fintype 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.