Basic definitions for graph pebbling

This file sets up the objects that should remain stable throughout the formalization: simple undirected graphs, pebbling distributions, legal pebbling moves, reachability, solvability, and optimality.

structure PebblingLean.Graph (V : Type u) : Type u

A simple undirected graph, kept intentionally small for the pebbling formalization.

• Adj : V → V → Prop

  The adjacency relation between vertices.

• symm {u v : V} : self.Adj u v → self.Adj v u

  Adjacency is symmetric.

• loopless (v : V) : ¬self.Adj v v

  The graph has no self-loops.

theorem PebblingLean.Graph.adj_comm {V : Type u} (G : Graph V) {u v : V} : G.Adj u v ↔ G.Adj v u

@[reducible, inline]

abbrev PebblingLean.Pebbling (V : Type u) : Type u

A pebbling distribution assigns a nonnegative number of pebbles to each vertex.

Equations

• PebblingLean.Pebbling V = (V → ℕ)

def PebblingLean.Pebbling.size {V : Type u} [Fintype V] (D : Pebbling V) : ℕ

The total number of pebbles in a finite distribution.

Equations

• D.size = ∑ v : V, D v

def PebblingLean.Pebbling.Dominates {V : Type u} (D E : Pebbling V) : Prop

Pointwise domination of pebbling distributions.

Equations

• D.Dominates E = ∀ (v : V), E v ≤ D v

@[simp]

theorem PebblingLean.Pebbling.size_zero {V : Type u} [Fintype V] : (size fun (x : V) => 0) = 0

theorem PebblingLean.Pebbling.le_size {V : Type u} [Fintype V] (D : Pebbling V) (v : V) : D v ≤ D.size

A single vertex count is bounded by the total size of a finite distribution.

def PebblingLean.Pebbling.moveDistribution {V : Type u} [DecidableEq V] (D : Pebbling V) (u v : V) : Pebbling V

The distribution obtained by moving two pebbles from u to one pebble at v. Legality of this operation is recorded separately in Move.

Equations

• D.moveDistribution u v x = if x = u then D x - 2 else if x = v then D x + 1 else D x

@[simp]

theorem PebblingLean.Pebbling.moveDistribution_apply_from {V : Type u} [DecidableEq V] (D : Pebbling V) {u v : V} : D.moveDistribution u v u = D u - 2

@[simp]

theorem PebblingLean.Pebbling.moveDistribution_apply_to {V : Type u} [DecidableEq V] (D : Pebbling V) {u v : V} (h : v ≠ u) : D.moveDistribution u v v = D v + 1

@[simp]

theorem PebblingLean.Pebbling.moveDistribution_apply_of_ne {V : Type u} [DecidableEq V] (D : Pebbling V) {u v x : V} (hxu : x ≠ u) (hxv : x ≠ v) : D.moveDistribution u v x = D x

theorem PebblingLean.Pebbling.moveDistribution_mono {V : Type u} [DecidableEq V] {D D' : Pebbling V} {u v : V} (huv : u ≠ v) (hdom : D'.Dominates D) : (D'.moveDistribution u v).Dominates (D.moveDistribution u v)

Performing the same move from a larger distribution gives a larger result.

def PebblingLean.Pebbling.Move {V : Type u} [DecidableEq V] (G : Graph V) (D E : Pebbling V) : Prop

One legal pebbling move: remove two pebbles from u and add one pebble to an adjacent vertex v.

Equations

• PebblingLean.Pebbling.Move G D E = ∃ (u : V) (v : V), G.Adj u v ∧ 2 ≤ D u ∧ E = D.moveDistribution u v

def PebblingLean.Pebbling.Reaches {V : Type u} [DecidableEq V] (G : Graph V) (D E : Pebbling V) : Prop

E is reachable from D by zero or more pebbling moves.

Equations

• PebblingLean.Pebbling.Reaches G D E = Relation.ReflTransGen (PebblingLean.Pebbling.Move G) D E

def PebblingLean.Pebbling.CanReachAtLeast {V : Type u} [DecidableEq V] (G : Graph V) (D : Pebbling V) (target : V) (T : ℕ) : Prop

Reach a target with at least T pebbles.

Equations

• PebblingLean.Pebbling.CanReachAtLeast G D target T = ∃ (E : PebblingLean.Pebbling V), PebblingLean.Pebbling.Reaches G D E ∧ T ≤ E target

def PebblingLean.Pebbling.CanReach {V : Type u} [DecidableEq V] (G : Graph V) (D : Pebbling V) (target : V) : Prop

A distribution can reach a target if some reachable distribution has at least one pebble on that target.

Equations

• PebblingLean.Pebbling.CanReach G D target = PebblingLean.Pebbling.CanReachAtLeast G D target 1

def PebblingLean.Pebbling.SolvableAtLeast {V : Type u} [DecidableEq V] (G : Graph V) (D : Pebbling V) (T : ℕ) : Prop

A distribution is T-solvable if it can move at least T pebbles to every target.

Equations

• PebblingLean.Pebbling.SolvableAtLeast G D T = ∀ (target : V), PebblingLean.Pebbling.CanReachAtLeast G D target T

def PebblingLean.Pebbling.Solvable {V : Type u} [DecidableEq V] (G : Graph V) (D : Pebbling V) : Prop

A distribution is solvable if it can reach every target vertex.

Equations

• PebblingLean.Pebbling.Solvable G D = PebblingLean.Pebbling.SolvableAtLeast G D 1

theorem PebblingLean.Pebbling.canReachAtLeast_zero {V : Type u} [DecidableEq V] (G : Graph V) (D : Pebbling V) (target : V) : CanReachAtLeast G D target 0

Reaching demand zero is automatic.

theorem PebblingLean.Pebbling.solvableAtLeast_zero {V : Type u} [DecidableEq V] (G : Graph V) (D : Pebbling V) : SolvableAtLeast G D 0

Every distribution is zero-demand solvable.

def PebblingLean.Pebbling.HasSolvableSize {V : Type u} [Fintype V] [DecidableEq V] (G : Graph V) (k : ℕ) : Prop

There is a solvable distribution of total size k.

Equations

• PebblingLean.Pebbling.HasSolvableSize G k = ∃ (D : PebblingLean.Pebbling V), D.size = k ∧ PebblingLean.Pebbling.Solvable G D

def PebblingLean.Pebbling.HasSolvableAtLeastSize {V : Type u} [Fintype V] [DecidableEq V] (G : Graph V) (T k : ℕ) : Prop

There is a T-solvable distribution of total size k.

Equations

• PebblingLean.Pebbling.HasSolvableAtLeastSize G T k = ∃ (D : PebblingLean.Pebbling V), D.size = k ∧ PebblingLean.Pebbling.SolvableAtLeast G D T

def PebblingLean.Pebbling.HasSolvableAtMostSize {V : Type u} [Fintype V] [DecidableEq V] (G : Graph V) (T k : ℕ) : Prop

There is a T-solvable distribution of total size at most k. This is the natural form for upper-bound constructions.

Equations

• PebblingLean.Pebbling.HasSolvableAtMostSize G T k = ∃ (D : PebblingLean.Pebbling V), D.size ≤ k ∧ PebblingLean.Pebbling.SolvableAtLeast G D T

def PebblingLean.Pebbling.MinOccupiedPileSize {V : Type u} (D : Pebbling V) (S : ℕ) : Prop

Every occupied pile in D has size at least S.

Equations

• D.MinOccupiedPileSize S = ∀ (v : V), D v ≠ 0 → S ≤ D v

def PebblingLean.Pebbling.supportSize {V : Type u} [Fintype V] (D : Pebbling V) : ℕ

Number of occupied vertices in a finite pebbling distribution.

Equations

• D.supportSize = {v : V | D v ≠ 0}.card

def PebblingLean.Pebbling.IsOptimalNumber {V : Type u} [Fintype V] [DecidableEq V] (G : Graph V) (k : ℕ) : Prop

A relational form of the optimal pebbling number: k is optimal if there is a solvable distribution with k pebbles, and none with fewer. This avoids choosing a numerical value before proving existence for the graph family under study.

Equations

• PebblingLean.Pebbling.IsOptimalNumber G k = (PebblingLean.Pebbling.HasSolvableSize G k ∧ ∀ l < k, ¬PebblingLean.Pebbling.HasSolvableSize G l)

def PebblingLean.Pebbling.IsOptimalDemandNumber {V : Type u} [Fintype V] [DecidableEq V] (G : Graph V) (T k : ℕ) : Prop

A relational form of the optimal T-pebbling number.

Equations

• PebblingLean.Pebbling.IsOptimalDemandNumber G T k = (PebblingLean.Pebbling.HasSolvableAtLeastSize G T k ∧ ∀ l < k, ¬PebblingLean.Pebbling.HasSolvableAtLeastSize G T l)

theorem PebblingLean.Pebbling.move_of_dominates {V : Type u} [DecidableEq V] {G : Graph V} {D E D' : Pebbling V} (hmove : Move G D E) (hdom : D'.Dominates D) : ∃ (E' : Pebbling V), Move G D' E' ∧ E'.Dominates E

A single move can be replayed from a dominating distribution.

theorem PebblingLean.Pebbling.reaches_of_dominates {V : Type u} [DecidableEq V] {G : Graph V} {D E D' : Pebbling V} (hreach : Reaches G D E) (hdom : D'.Dominates D) : ∃ (E' : Pebbling V), Reaches G D' E' ∧ E'.Dominates E

Any sequence of moves can be replayed from a dominating distribution.

theorem PebblingLean.Pebbling.canReachAtLeast_of_dominates {V : Type u} [DecidableEq V] {G : Graph V} {D D' : Pebbling V} {target : V} {T : ℕ} (hcan : CanReachAtLeast G D target T) (hdom : D'.Dominates D) : CanReachAtLeast G D' target T

Extra pebbles cannot hurt target reachability.

theorem PebblingLean.Pebbling.canReachAtLeast_mono {V : Type u} [DecidableEq V] {G : Graph V} {D : Pebbling V} {target : V} {T T' : ℕ} (hTT' : T' ≤ T) (hcan : CanReachAtLeast G D target T) : CanReachAtLeast G D target T'

If a distribution can reach a larger demand, it can reach any smaller demand.

theorem PebblingLean.Pebbling.solvableAtLeast_of_dominates {V : Type u} [DecidableEq V] {G : Graph V} {D D' : Pebbling V} {T : ℕ} (hsolv : SolvableAtLeast G D T) (hdom : D'.Dominates D) : SolvableAtLeast G D' T

Extra pebbles cannot hurt T-solvability.

theorem PebblingLean.Pebbling.solvableAtLeast_mono {V : Type u} [DecidableEq V] {G : Graph V} {D : Pebbling V} {T T' : ℕ} (hTT' : T' ≤ T) (hsolv : SolvableAtLeast G D T) : SolvableAtLeast G D T'

T-solvability implies any smaller demand.

theorem PebblingLean.Pebbling.solvable_of_solvableAtLeast {V : Type u} [DecidableEq V] {G : Graph V} {D : Pebbling V} {T : ℕ} (hT : 1 ≤ T) (hsolv : SolvableAtLeast G D T) : Solvable G D

A distribution that is T-solvable for T ≥ 1 is solvable in the usual one-pebble sense.

theorem PebblingLean.Pebbling.hasSolvableAtMostSize_mono_demand {V : Type u} [Fintype V] [DecidableEq V] {G : Graph V} {T T' k : ℕ} (hTT' : T' ≤ T) (h : HasSolvableAtMostSize G T k) : HasSolvableAtMostSize G T' k

A bounded-size construction for a larger demand also works for any smaller demand.

theorem PebblingLean.Pebbling.hasSolvableAtMostSize_mono_size {V : Type u} [Fintype V] [DecidableEq V] {G : Graph V} {T k k' : ℕ} (hkk' : k ≤ k') (h : HasSolvableAtMostSize G T k) : HasSolvableAtMostSize G T k'

A construction with size at most k is also a construction with any larger size bound.

theorem PebblingLean.Pebbling.size_add {V : Type u} [Fintype V] (D E : Pebbling V) : (D + E).size = D.size + E.size

The size of a sum of two finite distributions is the sum of their sizes.

theorem PebblingLean.Pebbling.sum_ite_nonzero_const {V : Type u} [Fintype V] (D : Pebbling V) (K : ℕ) : (∑ v : V, if D v = 0 then 0 else K) = D.supportSize * K

theorem PebblingLean.Pebbling.supportSize_mul_le_size_of_minOccupiedPileSize {V : Type u} [Fintype V] {D : Pebbling V} {S : ℕ} (hmin : D.MinOccupiedPileSize S) : D.supportSize * S ≤ D.size

If each occupied pile has at least S pebbles, then the number of occupied vertices times S is at most the total size.

theorem PebblingLean.Pebbling.supportSize_mul_minPileCost_le_size_mul {V : Type u} [Fintype V] {D : Pebbling V} {S K : ℕ} (hmin : D.MinOccupiedPileSize S) : D.supportSize * (S * K) ≤ D.size * K

Multiplicative form of the occupied-pile count bound, used in product recurrences.