Direct delivery along paths

This file formalizes the elementary deterministic fact used inside the upper bound: a pile of size T * 2^d at one end of a length-d path can deliver T pebbles to the other end.

inductive PebblingLean.Graph.Walk {V : Type u} (G : Graph V) : V → V → Type u

Walks in the custom graph structure used by this project.

• nil {V : Type u} {G : Graph V} (v : V) : G.Walk v v
• cons {V : Type u} {G : Graph V} {u v w : V} : G.Adj u v → G.Walk v w → G.Walk u w

def PebblingLean.Graph.Walk.length {V : Type u} (G : Graph V) {u v : V} : G.Walk u v → ℕ

Length of a walk.

Equations

• PebblingLean.Graph.Walk.length G (PebblingLean.Graph.Walk.nil u) = 0
• PebblingLean.Graph.Walk.length G (PebblingLean.Graph.Walk.cons a tail) = PebblingLean.Graph.Walk.length G tail + 1

def PebblingLean.Graph.Walk.append {V : Type u} (G : Graph V) {u v w : V} : G.Walk u v → G.Walk v w → G.Walk u w

Concatenate two walks.

Equations

• PebblingLean.Graph.Walk.append G (PebblingLean.Graph.Walk.nil u) tail = tail
• PebblingLean.Graph.Walk.append G (PebblingLean.Graph.Walk.cons h headTail) x✝ = PebblingLean.Graph.Walk.cons h (PebblingLean.Graph.Walk.append G headTail x✝)

@[simp]

theorem PebblingLean.Graph.Walk.length_append {V : Type u} (G : Graph V) {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : length G (append G p q) = length G p + length G q

def PebblingLean.Graph.Walk.reverse {V : Type u} (G : Graph V) {u v : V} : G.Walk u v → G.Walk v u

Reverse a walk in an undirected graph.

Equations

• One or more equations did not get rendered due to their size.
• PebblingLean.Graph.Walk.reverse G (PebblingLean.Graph.Walk.nil v) = PebblingLean.Graph.Walk.nil v

@[simp]

theorem PebblingLean.Graph.Walk.length_reverse {V : Type u} (G : Graph V) {u v : V} (p : G.Walk u v) : length G (reverse G p) = length G p

def PebblingLean.Pebbling.single {V : Type u} [DecidableEq V] (v : V) (k : ℕ) : Pebbling V

A distribution with k pebbles at one vertex and none elsewhere.

Equations

• PebblingLean.Pebbling.single v k x = if x = v then k else 0

@[simp]

theorem PebblingLean.Pebbling.single_apply_self {V : Type u} [DecidableEq V] (v : V) (k : ℕ) : single v k v = k

@[simp]

theorem PebblingLean.Pebbling.single_apply_ne {V : Type u} [DecidableEq V] {u v : V} (k : ℕ) (h : u ≠ v) : single v k u = 0

@[simp]

theorem PebblingLean.Pebbling.size_single {V : Type u} [Fintype V] [DecidableEq V] (v : V) (k : ℕ) : (single v k).size = k

def PebblingLean.Pebbling.twoPoint {V : Type u} [DecidableEq V] (u v : V) (ku kv : ℕ) : Pebbling V

A distribution supported on two distinct vertices. If the vertices are not distinct, the first branch takes precedence; the lemmas below use adjacent vertices, so they are distinct.

Equations

• PebblingLean.Pebbling.twoPoint u v ku kv x = if x = u then ku else if x = v then kv else 0

@[simp]

theorem PebblingLean.Pebbling.twoPoint_apply_left {V : Type u} [DecidableEq V] (u v : V) (ku kv : ℕ) : twoPoint u v ku kv u = ku

@[simp]

theorem PebblingLean.Pebbling.twoPoint_apply_right {V : Type u} [DecidableEq V] {u v : V} (ku kv : ℕ) (hvu : v ≠ u) : twoPoint u v ku kv v = kv

@[simp]

theorem PebblingLean.Pebbling.twoPoint_apply_ne {V : Type u} [DecidableEq V] {u v x : V} (ku kv : ℕ) (hxu : x ≠ u) (hxv : x ≠ v) : twoPoint u v ku kv x = 0

theorem PebblingLean.Pebbling.single_eq_twoPoint_right_zero {V : Type u} [DecidableEq V] {u v : V} (k : ℕ) (huv : u ≠ v) : single u k = twoPoint u v k 0

theorem PebblingLean.Pebbling.single_eq_twoPoint_left_zero {V : Type u} [DecidableEq V] {u v : V} (k : ℕ) (huv : u ≠ v) : single v k = twoPoint u v 0 k

theorem PebblingLean.Pebbling.twoPoint_edge_move {V : Type u} [DecidableEq V] {G : Graph V} {u v : V} (huv_adj : G.Adj u v) (k a : ℕ) : Move G (twoPoint u v (2 * (k + 1)) a) (twoPoint u v (2 * k) (a + 1))

One edge move transfers one pebble from the left support vertex to the right support vertex, consuming two pebbles on the left.

theorem PebblingLean.Pebbling.reaches_twoPoint_edge {V : Type u} [DecidableEq V] {G : Graph V} {u v : V} (huv_adj : G.Adj u v) (k a : ℕ) : Reaches G (twoPoint u v (2 * k) a) (twoPoint u v 0 (a + k))

Repeating the same edge move sends k pebbles across an edge from a pile of size 2*k, preserving any accumulator already present at the destination.

theorem PebblingLean.Pebbling.reaches_single_edge {V : Type u} [DecidableEq V] {G : Graph V} {u v : V} (huv_adj : G.Adj u v) (k : ℕ) : Reaches G (single u (2 * k)) (single v k)

A pile of 2*k pebbles at one endpoint of an edge can deliver k pebbles to the other endpoint.

theorem PebblingLean.Pebbling.canReachAtLeast_single_of_walk {V : Type u} [DecidableEq V] {G : Graph V} {u target : V} (walk : G.Walk u target) (T : ℕ) : CanReachAtLeast G (single u (T * 2 ^ Graph.Walk.length G walk)) target T

Direct delivery along a walk.

theorem PebblingLean.Pebbling.canReachAtLeast_of_walk_of_single_dominated {V : Type u} [DecidableEq V] {G : Graph V} {D : Pebbling V} {u target : V} (walk : G.Walk u target) {T : ℕ} (hdom : D.Dominates (single u (T * 2 ^ Graph.Walk.length G walk))) : CanReachAtLeast G D target T

Direct delivery is monotone in the initial distribution: extra pebbles away from the chosen starting pile cannot hurt.

theorem PebblingLean.Pebbling.move_add_right {V : Type u} [DecidableEq V] {G : Graph V} {D E A : Pebbling V} (hmove : Move G D E) : Move G (D + A) (E + A)

Moving from D to E can be done with an untouched extra distribution added everywhere.

theorem PebblingLean.Pebbling.reaches_add_right {V : Type u} [DecidableEq V] {G : Graph V} {D E A : Pebbling V} (hreach : Reaches G D E) : Reaches G (D + A) (E + A)

A whole pebbling sequence can be replayed with an untouched extra distribution added everywhere.

theorem PebblingLean.Pebbling.canReachAtLeast_add {V : Type u} [DecidableEq V] {G : Graph V} {D₁ D₂ : Pebbling V} {target : V} {T₁ T₂ : ℕ} (h₁ : CanReachAtLeast G D₁ target T₁) (h₂ : CanReachAtLeast G D₂ target T₂) : CanReachAtLeast G (D₁ + D₂) target (T₁ + T₂)

If two distributions can independently deliver T₁ and T₂ pebbles to the same target, their sum can deliver T₁ + T₂.